From f638c5ac7e9d100b8a93070b0648c496c6c901e0 Mon Sep 17 00:00:00 2001 From: Matthias Hutzler Date: Thu, 28 Sep 2023 16:29:47 +0200 Subject: [PATCH 1/7] delete this, as suggested by Emily --- src/hott/06-contractible.rzk.md | 18 ------------------ 1 file changed, 18 deletions(-) diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md index f33ed30c..02f4a5e5 100644 --- a/src/hott/06-contractible.rzk.md +++ b/src/hott/06-contractible.rzk.md @@ -412,24 +412,6 @@ separate hypothesis. ``` -For future reference we add a variable we can assume. - -```rzk -#assume weakfunext : WeakFunExt -``` - -Whenever a definition (implicitly) uses function extensionality, we write -`#!rzk uses (weakfunext)`. - -```rzk -#def call-weakfunext uses (weakfunext) - ( A : U ) - ( C : A → U) - ( f : (a : A) → is-contr (C a) ) - : (is-contr ( (a : A) → C a )) - := weakfunext A C f -``` - ## Singleton induction A type is contractible if and only if it has singleton induction. From 8419403e8fea5b4322f2afdb271069c5345d2a82 Mon Sep 17 00:00:00 2001 From: Matthias Hutzler Date: Thu, 28 Sep 2023 17:41:21 +0200 Subject: [PATCH 2/7] weakfunext-funext --- src/hott/06-contractible.rzk.md | 39 +++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md index 02f4a5e5..a469ffe3 100644 --- a/src/hott/06-contractible.rzk.md +++ b/src/hott/06-contractible.rzk.md @@ -407,11 +407,50 @@ separate hypothesis. #def WeakFunExt : U := ( A : U ) → (C : A → U) → + -- TODO: rename f (also below)? (f : (a : A) → is-contr (C a) ) → (is-contr ( (a : A) → C a )) ``` +Weak function extensionality implies function extensionality. + + +```rzk +-- TODO: delete +#assume hole : (A : U) → A + +#def funext-weakfunext + ( weakfunext : WeakFunExt ) + : FunExt + := hole FunExt +``` + +```rzk +-- TODO: better name? or inline this? +#def map-weakfunext-funext + (A : U) + (C : A → U) + (f : (a : A) → is-contr (C a)) + : (a : A) → C a + := + \ a → first (f a) + +#def weakfunext-funext + (funext : FunExt) + : WeakFunExt + := + ( \ A → \ C → \ f → + ( map-weakfunext-funext A C f , + ( \ (g : (a : A) → C a) → + ( eq-htpy funext + ( A) + ( C) + ( map-weakfunext-funext A C f) + ( g) + ( \ a → second (f a) (g a)))))) +``` + ## Singleton induction A type is contractible if and only if it has singleton induction. From 2b38f9035151c06ddb9818523730e1e376f531a0 Mon Sep 17 00:00:00 2001 From: Matthias Hutzler Date: Thu, 28 Sep 2023 17:52:57 +0200 Subject: [PATCH 3/7] name idea --- src/hott/06-contractible.rzk.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md index a469ffe3..b716fe3c 100644 --- a/src/hott/06-contractible.rzk.md +++ b/src/hott/06-contractible.rzk.md @@ -407,7 +407,7 @@ separate hypothesis. #def WeakFunExt : U := ( A : U ) → (C : A → U) → - -- TODO: rename f (also below)? + -- TODO: rename f to is-contr-C (also below)? (f : (a : A) → is-contr (C a) ) → (is-contr ( (a : A) → C a )) From 4132c1b6d42e95b19ef31508e69373915c6338e6 Mon Sep 17 00:00:00 2001 From: Matthias Hutzler Date: Fri, 29 Sep 2023 11:44:12 +0200 Subject: [PATCH 4/7] polish --- src/hott/06-contractible.rzk.md | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md index b716fe3c..f67e3ad4 100644 --- a/src/hott/06-contractible.rzk.md +++ b/src/hott/06-contractible.rzk.md @@ -426,6 +426,8 @@ Weak function extensionality implies function extensionality. := hole FunExt ``` +Function extensionality implies weak function extensionality. + ```rzk -- TODO: better name? or inline this? #def map-weakfunext-funext @@ -440,15 +442,15 @@ Weak function extensionality implies function extensionality. (funext : FunExt) : WeakFunExt := - ( \ A → \ C → \ f → - ( map-weakfunext-funext A C f , - ( \ (g : (a : A) → C a) → - ( eq-htpy funext - ( A) - ( C) - ( map-weakfunext-funext A C f) - ( g) - ( \ a → second (f a) (g a)))))) + \ A C f → + ( map-weakfunext-funext A C f , + ( \ (g : (a : A) → C a) → + ( eq-htpy funext + ( A) + ( C) + ( map-weakfunext-funext A C f) + ( g) + ( \ a → second (f a) (g a))))) ``` ## Singleton induction From c4405ed08206ab168068744b89cff3a752fc967c Mon Sep 17 00:00:00 2001 From: Matthias Hutzler Date: Fri, 29 Sep 2023 12:22:35 +0200 Subject: [PATCH 5/7] clean up --- src/hott/06-contractible.rzk.md | 31 ++++++++----------------------- 1 file changed, 8 insertions(+), 23 deletions(-) diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md index f67e3ad4..2570038c 100644 --- a/src/hott/06-contractible.rzk.md +++ b/src/hott/06-contractible.rzk.md @@ -407,50 +407,35 @@ separate hypothesis. #def WeakFunExt : U := ( A : U ) → (C : A → U) → - -- TODO: rename f to is-contr-C (also below)? - (f : (a : A) → is-contr (C a) ) → + (is-contr-C : (a : A) → is-contr (C a) ) → (is-contr ( (a : A) → C a )) ``` -Weak function extensionality implies function extensionality. - - -```rzk --- TODO: delete -#assume hole : (A : U) → A - -#def funext-weakfunext - ( weakfunext : WeakFunExt ) - : FunExt - := hole FunExt -``` - Function extensionality implies weak function extensionality. ```rzk --- TODO: better name? or inline this? -#def map-weakfunext-funext +#def map-for-weakfunext (A : U) (C : A → U) - (f : (a : A) → is-contr (C a)) + (is-contr-C : (a : A) → is-contr (C a)) : (a : A) → C a := - \ a → first (f a) + \ a → first (is-contr-C a) #def weakfunext-funext (funext : FunExt) : WeakFunExt := - \ A C f → - ( map-weakfunext-funext A C f , + \ A C is-contr-C → + ( map-for-weakfunext A C is-contr-C , ( \ (g : (a : A) → C a) → ( eq-htpy funext ( A) ( C) - ( map-weakfunext-funext A C f) + ( map-for-weakfunext A C is-contr-C) ( g) - ( \ a → second (f a) (g a))))) + ( \ a → second (is-contr-C a) (g a))))) ``` ## Singleton induction From 77fc08def4f80864e8a133ba28380bd77ba5f454 Mon Sep 17 00:00:00 2001 From: Matthias Hutzler Date: Fri, 29 Sep 2023 12:27:30 +0200 Subject: [PATCH 6/7] remove unusual annotation --- src/hott/06-contractible.rzk.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md index 2570038c..1d5e0ecf 100644 --- a/src/hott/06-contractible.rzk.md +++ b/src/hott/06-contractible.rzk.md @@ -429,7 +429,7 @@ Function extensionality implies weak function extensionality. := \ A C is-contr-C → ( map-for-weakfunext A C is-contr-C , - ( \ (g : (a : A) → C a) → + ( \ g → ( eq-htpy funext ( A) ( C) From 7f209039e0f2e381ed360f601850f72de83268db Mon Sep 17 00:00:00 2001 From: Matthias Hutzler Date: Mon, 2 Oct 2023 09:09:27 +0200 Subject: [PATCH 7/7] improve naming --- src/hott/06-contractible.rzk.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md index 1d5e0ecf..04aa5c54 100644 --- a/src/hott/06-contractible.rzk.md +++ b/src/hott/06-contractible.rzk.md @@ -415,7 +415,7 @@ separate hypothesis. Function extensionality implies weak function extensionality. ```rzk -#def map-for-weakfunext +#def map-weakfunext (A : U) (C : A → U) (is-contr-C : (a : A) → is-contr (C a)) @@ -428,12 +428,12 @@ Function extensionality implies weak function extensionality. : WeakFunExt := \ A C is-contr-C → - ( map-for-weakfunext A C is-contr-C , + ( map-weakfunext A C is-contr-C , ( \ g → ( eq-htpy funext ( A) ( C) - ( map-for-weakfunext A C is-contr-C) + ( map-weakfunext A C is-contr-C) ( g) ( \ a → second (is-contr-C a) (g a))))) ```