From 1c28c2e39a46e932df8008449e21b96123599297 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 24 Oct 2023 13:04:36 +0200 Subject: [PATCH 01/12] funExt is an equivalence. --- Cubical/Foundations/Equiv.agda | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda index c3a6e346db..2c12278bfa 100644 --- a/Cubical/Foundations/Equiv.agda +++ b/Cubical/Foundations/Equiv.agda @@ -316,3 +316,16 @@ isEquiv-isEquiv'-Iso f .leftInv p i .equiv-proof = p .equiv-proof isEquiv≃isEquiv' : (f : A → B) → isEquiv f ≃ isEquiv' f isEquiv≃isEquiv' f = isoToEquiv (isEquiv-isEquiv'-Iso f) + +-- funExt is an equivalence + +funExt≃ : {B : A → I → Type ℓ'} {f : (x : A) → B x i0} {g : (x : A) → B x i1} → + ((x : A) → PathP (B x) (f x) (g x)) ≃ PathP (λ i → (x : A) → B x i) f g +funExt≃ {A = A}{B = B} {f = f} {g = g} = isoToEquiv e + where + open Iso + e : Iso ((x : A) → PathP (B x) (f x) (g x)) (PathP (λ i → (x : A) → B x i) f g) + fun e p = funExt p + inv e p = funExt⁻ p + rightInv e p = refl + leftInv e p = refl From 7de91054413ce80686fb001c899ea13fc58dbbd5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 2 Nov 2023 13:32:03 +0100 Subject: [PATCH 02/12] Update Cubical/Foundations/Equiv.agda --- Cubical/Foundations/Equiv.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda index 2c12278bfa..38fbe86f99 100644 --- a/Cubical/Foundations/Equiv.agda +++ b/Cubical/Foundations/Equiv.agda @@ -317,7 +317,7 @@ isEquiv-isEquiv'-Iso f .leftInv p i .equiv-proof = p .equiv-proof isEquiv≃isEquiv' : (f : A → B) → isEquiv f ≃ isEquiv' f isEquiv≃isEquiv' f = isoToEquiv (isEquiv-isEquiv'-Iso f) --- funExt is an equivalence +-- The fact that funExt is an equivalence can be found in Cubical.Functions.FunExtEquiv funExt≃ : {B : A → I → Type ℓ'} {f : (x : A) → B x i0} {g : (x : A) → B x i1} → ((x : A) → PathP (B x) (f x) (g x)) ≃ PathP (λ i → (x : A) → B x i) f g From b93018cf39dab559072ba366aa0483b232ca7481 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 2 Nov 2023 13:32:08 +0100 Subject: [PATCH 03/12] Update Cubical/Foundations/Equiv.agda --- Cubical/Foundations/Equiv.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda index 38fbe86f99..fef7f76e32 100644 --- a/Cubical/Foundations/Equiv.agda +++ b/Cubical/Foundations/Equiv.agda @@ -319,7 +319,6 @@ isEquiv≃isEquiv' f = isoToEquiv (isEquiv-isEquiv'-Iso f) -- The fact that funExt is an equivalence can be found in Cubical.Functions.FunExtEquiv -funExt≃ : {B : A → I → Type ℓ'} {f : (x : A) → B x i0} {g : (x : A) → B x i1} → ((x : A) → PathP (B x) (f x) (g x)) ≃ PathP (λ i → (x : A) → B x i) f g funExt≃ {A = A}{B = B} {f = f} {g = g} = isoToEquiv e where From cba9ebc42eaafcd1aed970cf63aab8fda6f56bb0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 2 Nov 2023 13:32:15 +0100 Subject: [PATCH 04/12] Update Cubical/Foundations/Equiv.agda --- Cubical/Foundations/Equiv.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda index fef7f76e32..22f938d823 100644 --- a/Cubical/Foundations/Equiv.agda +++ b/Cubical/Foundations/Equiv.agda @@ -319,7 +319,6 @@ isEquiv≃isEquiv' f = isoToEquiv (isEquiv-isEquiv'-Iso f) -- The fact that funExt is an equivalence can be found in Cubical.Functions.FunExtEquiv - ((x : A) → PathP (B x) (f x) (g x)) ≃ PathP (λ i → (x : A) → B x i) f g funExt≃ {A = A}{B = B} {f = f} {g = g} = isoToEquiv e where open Iso From 83e4ba0c081744d75c9e07f5787634e6ef840509 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 2 Nov 2023 13:32:22 +0100 Subject: [PATCH 05/12] Update Cubical/Foundations/Equiv.agda --- Cubical/Foundations/Equiv.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda index 22f938d823..876c89029b 100644 --- a/Cubical/Foundations/Equiv.agda +++ b/Cubical/Foundations/Equiv.agda @@ -319,7 +319,6 @@ isEquiv≃isEquiv' f = isoToEquiv (isEquiv-isEquiv'-Iso f) -- The fact that funExt is an equivalence can be found in Cubical.Functions.FunExtEquiv -funExt≃ {A = A}{B = B} {f = f} {g = g} = isoToEquiv e where open Iso e : Iso ((x : A) → PathP (B x) (f x) (g x)) (PathP (λ i → (x : A) → B x i) f g) From b28b4e8fb371f85a11c090ad56debf8fc3d89437 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 2 Nov 2023 13:32:27 +0100 Subject: [PATCH 06/12] Update Cubical/Foundations/Equiv.agda --- Cubical/Foundations/Equiv.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda index 876c89029b..5d9fbe3726 100644 --- a/Cubical/Foundations/Equiv.agda +++ b/Cubical/Foundations/Equiv.agda @@ -319,7 +319,6 @@ isEquiv≃isEquiv' f = isoToEquiv (isEquiv-isEquiv'-Iso f) -- The fact that funExt is an equivalence can be found in Cubical.Functions.FunExtEquiv - where open Iso e : Iso ((x : A) → PathP (B x) (f x) (g x)) (PathP (λ i → (x : A) → B x i) f g) fun e p = funExt p From c6e4d6954124297aeb37d4cb03eb499ad23b11cd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 2 Nov 2023 13:32:33 +0100 Subject: [PATCH 07/12] Update Cubical/Foundations/Equiv.agda --- Cubical/Foundations/Equiv.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda index 5d9fbe3726..5783bc7b17 100644 --- a/Cubical/Foundations/Equiv.agda +++ b/Cubical/Foundations/Equiv.agda @@ -319,7 +319,6 @@ isEquiv≃isEquiv' f = isoToEquiv (isEquiv-isEquiv'-Iso f) -- The fact that funExt is an equivalence can be found in Cubical.Functions.FunExtEquiv - open Iso e : Iso ((x : A) → PathP (B x) (f x) (g x)) (PathP (λ i → (x : A) → B x i) f g) fun e p = funExt p inv e p = funExt⁻ p From 3c6caf95ac2cad09516a17398c62f8b27e5e60c8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 2 Nov 2023 13:32:38 +0100 Subject: [PATCH 08/12] Update Cubical/Foundations/Equiv.agda --- Cubical/Foundations/Equiv.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda index 5783bc7b17..64b999dd9b 100644 --- a/Cubical/Foundations/Equiv.agda +++ b/Cubical/Foundations/Equiv.agda @@ -319,7 +319,6 @@ isEquiv≃isEquiv' f = isoToEquiv (isEquiv-isEquiv'-Iso f) -- The fact that funExt is an equivalence can be found in Cubical.Functions.FunExtEquiv - e : Iso ((x : A) → PathP (B x) (f x) (g x)) (PathP (λ i → (x : A) → B x i) f g) fun e p = funExt p inv e p = funExt⁻ p rightInv e p = refl From f94ab37ccc0bebb09fd120634e5f4114919ef7b7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 2 Nov 2023 13:32:43 +0100 Subject: [PATCH 09/12] Update Cubical/Foundations/Equiv.agda --- Cubical/Foundations/Equiv.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda index 64b999dd9b..57eee40d33 100644 --- a/Cubical/Foundations/Equiv.agda +++ b/Cubical/Foundations/Equiv.agda @@ -319,7 +319,6 @@ isEquiv≃isEquiv' f = isoToEquiv (isEquiv-isEquiv'-Iso f) -- The fact that funExt is an equivalence can be found in Cubical.Functions.FunExtEquiv - fun e p = funExt p inv e p = funExt⁻ p rightInv e p = refl leftInv e p = refl From a07d0920a196972203d6e523cb70e4bb94c67f0f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 2 Nov 2023 13:32:48 +0100 Subject: [PATCH 10/12] Update Cubical/Foundations/Equiv.agda --- Cubical/Foundations/Equiv.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda index 57eee40d33..c32f7ebbe8 100644 --- a/Cubical/Foundations/Equiv.agda +++ b/Cubical/Foundations/Equiv.agda @@ -319,6 +319,5 @@ isEquiv≃isEquiv' f = isoToEquiv (isEquiv-isEquiv'-Iso f) -- The fact that funExt is an equivalence can be found in Cubical.Functions.FunExtEquiv - inv e p = funExt⁻ p rightInv e p = refl leftInv e p = refl From 2c15a2d2ca81f621e967381981fb97a1173c842b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 2 Nov 2023 13:32:53 +0100 Subject: [PATCH 11/12] Update Cubical/Foundations/Equiv.agda --- Cubical/Foundations/Equiv.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda index c32f7ebbe8..cb8e55fc58 100644 --- a/Cubical/Foundations/Equiv.agda +++ b/Cubical/Foundations/Equiv.agda @@ -319,5 +319,4 @@ isEquiv≃isEquiv' f = isoToEquiv (isEquiv-isEquiv'-Iso f) -- The fact that funExt is an equivalence can be found in Cubical.Functions.FunExtEquiv - rightInv e p = refl leftInv e p = refl From c413dad89f3aadcc151e08e8b25db80027dbec5f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 2 Nov 2023 13:33:00 +0100 Subject: [PATCH 12/12] Update Cubical/Foundations/Equiv.agda --- Cubical/Foundations/Equiv.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda index cb8e55fc58..0529733212 100644 --- a/Cubical/Foundations/Equiv.agda +++ b/Cubical/Foundations/Equiv.agda @@ -319,4 +319,3 @@ isEquiv≃isEquiv' f = isoToEquiv (isEquiv-isEquiv'-Iso f) -- The fact that funExt is an equivalence can be found in Cubical.Functions.FunExtEquiv - leftInv e p = refl