namespace http://cds.omdoc.org/urtheories❚

import lf scala://lf.mmt.kwarc.info❚

theory Bool =
  include ?TermsTypesKinds ❙
  BOOL  : type❙
  TRUE  : BOOL❙
  FALSE  : BOOL❙
❚

theory Ded : ?LF =
  include ?Bool ❙
  
  DED   : BOOL ⟶ type❘ # DED 1 prec -5 ❘ role Judgment❙
  rule lf?TermIrrelevanceRule (DED)❙
  rule lf?PiIrrelevanceRule ❙
  
  TRUEI : DED TRUE❙
❚

//   dependently-typed higher-order logic, i.e., LF with booleans and equality❚
theory DHOL : ?PLF =
  include ?Ded ❙
  
  EQUAL : {a:type} a ⟶ a ⟶ BOOL ❘ # 2 EQ 3 prec 5❘role Eq❙
  NOTEQUAL : {a:type} a ⟶ a ⟶ BOOL ❘ # 2 NEQ 3 prec 5❙
  CONTRA : type ❘= DED FALSE❙
  
// if : {a:type} bool ⟶ a ⟶ a ⟶ a❙

  REFL  : {A,X:A} DED X EQ X  ❙
  SYM   : {A,X:A,Y} DED X EQ Y ⟶ DED Y EQ X❘# SYM 4❙
  TRANS : {A,X:A,Y,Z} DED X EQ Y ⟶ DED Y EQ Z ⟶ DED X EQ Z❘# 5 TRANS 6 ❙
  
  CONG : {A, B, X, Y: A} DED X EQ Y ⟶ {F: A ⟶ B} DED (F X) EQ (F Y)❘# 5 CONG 6❙
❚

theory DHOL2 : ?PLF =
  bool  : type ❙
  equal : {A:type} A ⟶ A ⟶ bool ❘ # 2 ≐ 3 prec 5 ❙

  ded  : bool ⟶ type ❘ # ⊦ 1 prec -5 ❙
  refl  : {A,X:A} ⊦ X ≐ X ❘ # refl %I1 %I2 ❙
  cong : {A, B: type} {F: A ⟶ B} {X, Y: A} ⊦ X ≐ Y ⟶ ⊦ (F X) ≐ (F Y) ❘ # congI 3 6 ❙

  extensionality : {A:type,B:A ⟶ type}{F:{x:A} B x, G:{x:A} B x} ({x: A} ⊦ F x ≐ G x) ⟶ ⊦ F ≐ G ❘ # ext 5 ❙
  eqDed    : {B1,B2:bool} ⊦ B1 ≐ B2 ⟶ ⊦ B1 ⟶ ⊦ B2 ❘ # eqded 3 4❙
  eqI    : {B1,B2:bool} (⊦ B1 ⟶ ⊦ B2) ⟶ (⊦ B2 ⟶ ⊦ B1) ⟶ ⊦ (B1 ≐ B2) ❘ # eqI 3 4 ❙

  symmetry : {A : type}{a,b : A} ⊦ a ≐ b ⟶ ⊦ b ≐ a ❘ = [A][a,b][p] eqded (congI ([x] x ≐ a) p) refl ❘ # symm 4 ❙
  eqFun : {A : type,B : type}{F,G : A ⟶ B} ⊦ F ≐ G ⟶ {a} ⊦ F a ≐ G a ❘ = [A,B][F,G][p][a] congI ([H: A ⟶ B] H a) p ❘# eqfun 5 6 ❙

  true : bool ❘ = ([x:bool] x) ≐ ([x:bool] x) ❙
  trueI : ⊦ true ❘ = refl ❙

  forall : {A:type} (A ⟶ bool) ⟶ bool ❘ = [A,P] P ≐ ([x:A] true) ❘ # ∀ 2 ❙

  forallI : {A:type, P : A ⟶ bool}({x} ⊦ P x) ⟶ ⊦ ∀[x] P x ❘
    = [A,P][p] ext ([x: A] eqI ([pf: ⊦ P x] trueI) ([pt: ⊦ true] p x)) ❙
  forallE : {A:type, P : A ⟶ bool} (⊦ ∀[x]P x) ⟶ {a} ⊦ P a ❘
    = [A,P][p][a] eqded (eqfun (symm p) a) trueI ❙
❚

theory Option : ?PLF =
  OPTION : type ⟶ type ❙
	NONE : {a:type} OPTION a ❙  
	SOME : {a:type} a ⟶ OPTION a ❙
	MAP : {a: type, b: type} (a ⟶ b) ⟶ OPTION b ❙
❚