example 3.1.6

src/HottBook/Chapter2.lagda.md

@@ -12,7 +12,7 @@ open import HottBook.Chapter2Lemma231 public
 
 private
   variable
-    l : Level
+    l l2 : Level
 ```
 
 </details>
@@ -625,8 +625,8 @@ postulate
 ### Lemma 2.9.2
 
 ```
-happly : {A B : Set l}
-  → {f g : A → B}
+happly : {A : Set l} {B : A → Set l2}
+  → {f g : (x : A) → B x}
   → (p : f ≡ g)
   → (x : A)
   → f x ≡ g x
@@ -636,11 +636,23 @@ happly {A} {B} {f} {g} p x = ap (λ h → h x) p
 ### Axiom 2.9.3 (Function extensionality)
 
 ```
-postulate
-  funext : ∀ {l l2} {A : Set l} {B : A → Set l2}
-    → {f g : (x : A) → B x}
-    → ((x : A) → f x ≡ g x)
-    → f ≡ g
+module axiom2∙9∙3 where
+  private
+    variable
+      A : Set l
+      B : A → Set l2
+      f g : (x : A) → B x
+
+  postulate
+    funext : ((x : A) → f x ≡ g x) → f ≡ g
+    propositional-computation : (h : (x : A) → f x ≡ g x) → happly (funext h) ≡ h
+    propositional-uniqueness : (p : f ≡ g) → funext (happly p) ≡ p
+
+  happly-isequiv : isequiv (happly {l} {l2} {A} {B} {f} {g})
+  happly-isequiv = qinv-to-isequiv (mkQinv funext propositional-computation propositional-uniqueness)
+
+  happly-equiv : (f ≡ g) ≃ ((x : A) → f x ≡ g x)
+  happly-equiv = happly , happly-isequiv
 ```
 
 ### Equation 2.9.4

src/HottBook/Chapter3.lagda.md

@@ -65,11 +65,25 @@ TODO: DO this without path induction
 
 ```
 example3∙1∙6 : {A : Set} {B : A → Set} → ((x : A) → isSet (B x)) → isSet ((x : A) → B x)
--- example3∙1∙6 func f g p q =
---   let
---     wtf : p ≡ funext (λ x → happly p x)
---     wtf = refl
---   in {!   !}
+example3∙1∙6 {A} Bset f g p q =
+  let
+    open axiom2∙9∙3
+
+    p' = funext λ x → happly p x
+    q' = funext λ x → happly q x
+
+    p≡p' : p ≡ p'
+    p≡p' = sym (propositional-uniqueness p)
+
+    q≡q' : q ≡ q'
+    q≡q' = sym (propositional-uniqueness q)
+
+    lol : (x : A) → happly p x ≡ happly q x
+    lol x = Bset x (f x) (g x) (happly p x) (happly q x)
+
+    lol2 : happly p ≡ happly q
+    lol2 = funext lol
+  in sym (propositional-uniqueness p) ∙ ap funext lol2 ∙ (propositional-uniqueness q)
 ```
 
 ### Definition 3.1.7
@@ -293,6 +307,7 @@ example3∙6∙1 {A} {B} Aprop Bprop =
 ```
 example3∙6∙2 : {A : Set} {B : A → Set} → ((x : A) → isProp (B x)) → isProp ((x : A) → B x)
 example3∙6∙2 {A} {B} allProps = λ f g → funext λ x → allProps x (f x) (g x)
+  where open axiom2∙9∙3
 ```
 
 ## 3.7 Propositional truncation