From 327e2f84f266da3e2d846d2908c78584a4e26254 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Mon, 22 Jul 2024 22:12:26 +0200 Subject: [PATCH 1/7] weak funext implies funext --- src/hott/08-families-of-maps.rzk.md | 130 ++++++++++++++++++++++++++++ 1 file changed, 130 insertions(+) diff --git a/src/hott/08-families-of-maps.rzk.md b/src/hott/08-families-of-maps.rzk.md index d9006552..4a1898f8 100644 --- a/src/hott/08-families-of-maps.rzk.md +++ b/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 From 8bf2fbe5749b85b20661cbaefdea35497aed7191 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis <116834840+thchatzidiamantis@users.noreply.github.com> Date: Tue, 23 Jul 2024 08:25:09 +0200 Subject: [PATCH 2/7] Update src/hott/08-families-of-maps.rzk.md Co-authored-by: Nikolai Kudasov --- src/hott/08-families-of-maps.rzk.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/hott/08-families-of-maps.rzk.md b/src/hott/08-families-of-maps.rzk.md index 4a1898f8..f9150b16 100644 --- a/src/hott/08-families-of-maps.rzk.md +++ b/src/hott/08-families-of-maps.rzk.md @@ -789,8 +789,8 @@ contractible. 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. +direction. We can then prove a cycle of implications between `#!rzk FunExt`, `#!rzk NaiveFunExt` +and `#!rzk WeakFunExt`. ```rzk #def NaiveFunExt From ecf426a973974a950d624cf3b29bb14aaebf2d2d Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Tue, 23 Jul 2024 08:31:26 +0200 Subject: [PATCH 3/7] formatting --- src/hott/08-families-of-maps.rzk.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/hott/08-families-of-maps.rzk.md b/src/hott/08-families-of-maps.rzk.md index f9150b16..d37b657d 100644 --- a/src/hott/08-families-of-maps.rzk.md +++ b/src/hott/08-families-of-maps.rzk.md @@ -789,8 +789,8 @@ contractible. 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 `#!rzk FunExt`, `#!rzk NaiveFunExt` -and `#!rzk WeakFunExt`. +direction. We can then prove a cycle of implications between `#!rzk FunExt`, +`#!rzk NaiveFunExt` and `#!rzk WeakFunExt`. ```rzk #def NaiveFunExt From e6251e77bd3edac01479a9c86deaaaac0da1b383 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Tue, 23 Jul 2024 08:38:29 +0200 Subject: [PATCH 4/7] formatting --- src/hott/08-families-of-maps.rzk.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/hott/08-families-of-maps.rzk.md b/src/hott/08-families-of-maps.rzk.md index d37b657d..67980ab1 100644 --- a/src/hott/08-families-of-maps.rzk.md +++ b/src/hott/08-families-of-maps.rzk.md @@ -787,9 +787,9 @@ contractible. 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 `#!rzk FunExt`, +The proof of `weakfunext-funext` from `06-contractible.rzk` works with a version +of function extensionality only requiring the map in the converse direction. We +can then prove a cycle of implications between `#!rzk FunExt`, `#!rzk NaiveFunExt` and `#!rzk WeakFunExt`. ```rzk From 302e87244d88fb5563ac0f38f8730467248071a4 Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Thu, 25 Jul 2024 13:31:45 +0200 Subject: [PATCH 5/7] minor formatting fix --- src/hott/08-families-of-maps.rzk.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/hott/08-families-of-maps.rzk.md b/src/hott/08-families-of-maps.rzk.md index 67980ab1..dfaaa619 100644 --- a/src/hott/08-families-of-maps.rzk.md +++ b/src/hott/08-families-of-maps.rzk.md @@ -637,7 +637,6 @@ This allows us to apply "based path induction" to a family satisfying the fundamental theorem: ```rzk --- Please suggest a better name. #def ind-based-path ( familyequiv : (z : A) → (is-equiv (a = z) (B z) (f z))) ( P : (z : A) → B z → U) @@ -696,7 +695,7 @@ contractible. ## Weak function extensionality implies function extensionality -```rzk title"Rijke, 13.1" +```rzk title="Rijke, 13.1" #def prod-eq-pair-dhomotopy ( A : U) ( C : A → U) From 0ffbec61b88052808bd4c5b177da74eca8c49dbf Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Thu, 25 Jul 2024 16:45:27 +0200 Subject: [PATCH 6/7] exposition --- src/hott/08-families-of-maps.rzk.md | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/src/hott/08-families-of-maps.rzk.md b/src/hott/08-families-of-maps.rzk.md index dfaaa619..fb65a59b 100644 --- a/src/hott/08-families-of-maps.rzk.md +++ b/src/hott/08-families-of-maps.rzk.md @@ -695,7 +695,15 @@ contractible. ## Weak function extensionality implies function extensionality -```rzk title="Rijke, 13.1" +Using the fundamental theorem of identity types, we prove the converse of +`weakfunext-funext`, so we now know that `#!rzk FunExt` is logically equivalent +to `#!rzk WeakFunExt`. We follow the proof in Rijke, section 13.1. + +We first fix one of the two functions and show that `#!rzk WeakFunExt` implies a +version of function extensionality that asserts that a type of "maps together +with homotopies" is contractible. + +```rzk #def prod-eq-pair-dhomotopy ( A : U) ( C : A → U) @@ -765,7 +773,12 @@ contractible. ( A) ( \ x → Σ (c : (C x)) , (f x =_{C x} c)) ( \ x → is-contr-based-paths (C x) (f x))) +``` + +We now use the fundamental theorem of identity types to go from the version for +a fixed f to the total `#!rzk FunExt` axiom. +```rzk #def funext-weirdfunext ( weirdfunext : WeirdFunExt) : FunExt From 4f3b195d2113f6aea0339ae808dd971b8704702a Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Tue, 30 Jul 2024 11:50:40 +0200 Subject: [PATCH 7/7] renaming --- src/hott/08-families-of-maps.rzk.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/hott/08-families-of-maps.rzk.md b/src/hott/08-families-of-maps.rzk.md index fb65a59b..b3656e4a 100644 --- a/src/hott/08-families-of-maps.rzk.md +++ b/src/hott/08-families-of-maps.rzk.md @@ -704,7 +704,7 @@ version of function extensionality that asserts that a type of "maps together with homotopies" is contractible. ```rzk -#def prod-eq-pair-dhomotopy +#def components-dhomotopy ( A : U) ( C : A → U) ( f : (x : A) → C x) @@ -718,7 +718,7 @@ with homotopies" is contractible. ( \ x → ( g x , H x)) -#def has-retraction-prod-eq-pair-dhomotopy +#def has-retraction-components-dhomotopy ( A : U) ( C : A → U) ( f : (x : A) → C x) @@ -728,13 +728,13 @@ with homotopies" is contractible. ( ( x : A) → ( Σ ( c : (C x)) , ( f x =_{C x} c))) - ( prod-eq-pair-dhomotopy A C f) + ( components-dhomotopy A C f) := ( ( \ G → ( \ x → first (G x) , \ x → second (G x))) , \ x → refl) -#def is-retract-prod-eq-pair-dhomotopy +#def is-retract-components-dhomotopy ( A : U) ( C : A → U) ( f : (x : A) → C x) @@ -745,8 +745,8 @@ with homotopies" is contractible. → ( Σ ( c : (C x)) , ( f x =_{C x} c))) := - ( prod-eq-pair-dhomotopy A C f - , has-retraction-prod-eq-pair-dhomotopy A C f) + ( components-dhomotopy A C f + , has-retraction-components-dhomotopy A C f) #def WeirdFunExt : U @@ -768,7 +768,7 @@ with homotopies" is contractible. ( ( x : A) → ( Σ ( c : (C x)) , ( f x =_{C x} c))) - ( is-retract-prod-eq-pair-dhomotopy A C f) + ( is-retract-components-dhomotopy A C f) ( weakfunext ( A) ( \ x → Σ (c : (C x)) , (f x =_{C x} c))