extensionalities

encodings/bool_hol.lp

@@ -31,3 +31,5 @@ set infix 2 "=" ≔ eq
 set builtin "eq" ≔ eq // FIXME emacs indentation
 
 rule ε ($x = $y) ↪ Πp: η (_ ~> bool), ε (p $x) → ε (p $y)
+
+definition iff P Q ≔ (P ⊃ (λ_, Q)) ∧ ((λ_, Q ⊃ (λ_, P)))

encodings/builtins.lp

@@ -23,3 +23,6 @@ constant symbol str_cons: η {|!Number!|} → η {|!String!|} → η {|!String!|
 
 set declared "∃"
 definition ∃ {T: Set} (P: η T → η bool) ≔ ¬ (∀ (λx, ¬ (P x)))
+
+symbol propositional_extensionality:
+  ε (∀ {bool} (λp, (∀ {bool} (λq, (iff p q) ⊃ (λ_, eq {bool} p q)))))

prelude/functions.lp

@@ -7,9 +7,10 @@ require open personoj.prelude.logic
 // functions [D, R: TYPE]
 //
 
-// symbol
-// extensionality_postulate (D R: Term uType) (f g: Term (D ~> R))
-// : Term (biff (forall (λx: Term D, f x = g ) (f = g)))
+symbol extensionality_postulate:
+  ε (∀B (λD, ∀B (λR,
+                 ∀ (λf: η (D ~> R),
+                    ∀ (λg: η (D ~> R), iff (∀ (λx, f x = g x)) (f = g))))))
 
 // definition {|injective?|} {D} {R} (f: Term (D ~> R)) ≔
 //   forall (λx1, forall (λx2, imp (f x1 = f x2) (x1 = x2)))