Weak FunExt implies FunExt

src/hott/08-families-of-maps.rzk.md

@@ -694,6 +694,136 @@ contractible.
       ( \ x → second (familyequiv x))))
 ```
 
+## Weak function extensionality implies function extensionality
+
+```rzk title"Rijke, 13.1"
+#def prod-eq-pair-dhomotopy
+  ( A : U)
+  ( C : A → U)
+  ( f : (x : A) → C x)
+  : ( Σ ( g : (x : A) → C x)
+      , ( dhomotopy A C f g))
+  → ( ( x : A)
+    → ( Σ ( c : (C x))
+      , ( f x =_{C x} c)))
+  :=
+    \ (g , H) →
+      ( \ x →
+        ( g x , H x))
+
+#def has-retraction-prod-eq-pair-dhomotopy
+  ( A : U)
+  ( C : A → U)
+  ( f : (x : A) → C x)
+  : has-retraction
+      ( Σ ( g : (x : A) → C x)
+        , ( dhomotopy A C f g))
+      ( ( x : A)
+        → ( Σ ( c : (C x))
+          , ( f x =_{C x} c)))
+      ( prod-eq-pair-dhomotopy A C f)
+  :=
+    ( ( \ G →
+        ( \ x → first (G x) , \ x → second (G x)))
+    , \ x → refl)
+
+#def is-retract-prod-eq-pair-dhomotopy
+  ( A : U)
+  ( C : A → U)
+  ( f : (x : A) → C x)
+  : is-retract-of
+      ( Σ ( g : (x : A) → C x)
+        , ( dhomotopy A C f g))
+      ( ( x : A)
+        → ( Σ ( c : (C x))
+          , ( f x =_{C x} c)))
+  :=
+    ( prod-eq-pair-dhomotopy A C f
+    , has-retraction-prod-eq-pair-dhomotopy A C f)
+
+#def WeirdFunExt
+  : U
+  :=
+    ( A : U) → (C : A → U)
+  → ( f : (x : A) → C x)
+  → is-contr
+      ( Σ ( g : (x : A) → C x)
+        , ( dhomotopy A C f g))
+
+#def weirdfunext-weakfunext
+  ( weakfunext : WeakFunExt)
+  : WeirdFunExt
+  :=
+    \ A C f →
+      is-contr-is-retract-of-is-contr
+        ( Σ ( g : (x : A) → C x)
+          , ( dhomotopy A C f g))
+        ( ( x : A)
+          → ( Σ ( c : (C x))
+              , ( f x =_{C x} c)))
+        ( is-retract-prod-eq-pair-dhomotopy A C f)
+        ( weakfunext
+          ( A)
+          ( \ x → Σ (c : (C x)) , (f x =_{C x} c))
+          ( \ x → is-contr-based-paths (C x) (f x)))
+
+#def funext-weirdfunext
+  ( weirdfunext : WeirdFunExt)
+  : FunExt
+  :=
+    \ A C f g →
+      are-equiv-from-paths-is-contr-total
+        ( ( x : A) → C x)
+        ( f)
+        ( \ h → dhomotopy A C f h)
+        ( \ h → htpy-eq A C f h)
+        ( weirdfunext A C f)
+        ( g)
+
+#def funext-weakfunext
+  ( weakfunext : WeakFunExt)
+  : FunExt
+  :=
+    funext-weirdfunext (weirdfunext-weakfunext weakfunext)
+```
+
+The proof of `weakfunext-funext` from `06-contractible.rzk` works with a weaker
+version of function extensionality only requiring the map in the converse
+direction. We can then prove a cycle of implications between FunExt, NaiveFunExt
+and WeakFunExt.
+
+```rzk
+#def NaiveFunExt
+  : U
+  :=
+    ( A : U) → (C : A → U)
+  → ( f : (x : A) → C x)
+  → ( g : (x : A) → C x)
+  → ( p : (x : A) → f x = g x)
+  → ( f = g)
+
+#def naivefunext-funext
+  ( funext : FunExt)
+  : NaiveFunExt
+  :=
+    \ A C f g p →
+      eq-htpy funext A C f g p
+
+#def weakfunext-naivefunext
+  ( naivefunext : NaiveFunExt)
+  : WeakFunExt
+  :=
+    \ A C is-contr-C →
+      ( map-weakfunext A C is-contr-C
+      , ( \ g →
+          ( naivefunext
+            ( A)
+            ( C)
+            ( map-weakfunext A C is-contr-C)
+            ( g)
+          ( \ a → second (is-contr-C a) (g a)))))
+```
+
 ## Maps over product types
 
 For later use, we specialize the previous results to the case of a family of