namespace latin:/❚

fixmeta ur:?LF❚

theory InternalEquality =
  include ?InternalLogic❙
  include ?TypedEquality❙
  include ?SimpleFunctions❙
  equalConstant : {A} tm A → (A → bool)❘= [A]λ[x]λ[y]x≐y❙
❚

theory PropositionalExtensionality =
  include ?InternalEquality❙
  propext: {F,G} (⊦ F ⟶ ⊦ G) ⟶ (⊦ G ⟶ ⊦ F) ⟶ ⊦ F≐G❙
❚

theory IHOL =
  include ?InternalEquality❙
  include ?ISFOL❙
 ❚

theory IHOLND =
  include ?InternalEquality❙
  include ?TypedEqualityND❙
  include ?ISFOLND❙
  include ?PropositionalExtensionality❙  
 ❚

theory HOL =
  include ?IHOL❙
❚

theory HOLND =
  include ?HOL❙
  include ?IHOLND❙
  include ?SFOLND❙
  include ?SimpleFunctionsEta❙
  
  eq_equiv: {F,G} ⊦F≐G ⟶ ⊦F⇔G❘= [F,G,p] equivI ([q] p congP ([u]u) q) ([q] (p sym) congP ([u]u) q)❙
  equiv_eq: {F,G} ⊦F⇔G ⟶ ⊦F≐G❘= [F,G,p] propext ([q] p equivEl q) ([q] p equivEr q)❙
❚

theory PowerHOLND =
  include ?HOLND❙
  realize powertypes?PowerTypes❙

  power = [a] a → bool❙
  filter = [A,P] λ P❙
  in = [A,x,S] S @ x❙
  compute = [A,P,x] eq_equiv simpbeta❙
  expand = [A,S] eta sym❙
❚