From da844295d8ed4f2f56fd3ca859aedfd0469d4c2c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Thomas=20Wilskow=20Thorbj=C3=B8rnsen?= Date: Tue, 19 Nov 2024 22:59:40 -0500 Subject: [PATCH 1/9] Prove theorem 5.8.2 --- contrib/HoTTBook.v | 12 ++++++ theories/PathAny.v | 92 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 104 insertions(+) diff --git a/contrib/HoTTBook.v b/contrib/HoTTBook.v index 736c8330886..18cadbd7cd6 100644 --- a/contrib/HoTTBook.v +++ b/contrib/HoTTBook.v @@ -769,8 +769,20 @@ Definition Book_4_9_5 := @HoTT.Metatheory.FunextVarieties.WeakFunext_implies_Fun (* ================================================== thm:identity-systems *) (** Theorem 5.8.2 *) +Definition Book_5_8_2_i_implies_iii := @HoTT.PathAny.equiv_transport_IsIdentitySystem. +Definition Book_5_8_2_iii_implies_i {A} {a0 : A} {X : A -> Type} (x0 : X a0) + (e : forall (a : A), IsEquiv (fun p : a0 = a => transport X p x0)) + (P : forall (b : A), X b -> Type) + (r : P a0 x0) + := @HoTT.Basics.Equivalences.equiv_path_ind A a0 X + (fun a => @Build_Equiv _ _ _ (e a)) P r. + +Definition Book_5_8_2_iii_implies_iv := @HoTT.PathAny.contr_sigma_refl_rel. Definition Book_5_8_2_iv_implies_iii := @HoTT.PathAny.equiv_path_from_contr. +Definition Book_5_8_2_i_implies_ii := @HoTT.PathAny.contr_pfammap_identitysystem. +Definition Book_5_8_2_ii_implies_iii := @HoTT.PathAny.equiv_path_contr_pfammap. + (* ================================================== thm:ML-identity-systems *) (** Theorem 5.8.4 *) diff --git a/theories/PathAny.v b/theories/PathAny.v index d4b302acb53..d78d81a7ae2 100644 --- a/theories/PathAny.v +++ b/theories/PathAny.v @@ -1,4 +1,5 @@ Require Import Basics Types. +Require Import HoTT.Tactics. (** A nice method for proving characterizations of path-types of nested sigma-types, due to Rijke. *) @@ -79,3 +80,94 @@ Ltac contr_sigsig a c := (** For examples of the use of this tactic, see for instance [Factorization] and [Idempotents]. *) +(** Given that some type family [R] is fiber-wise equivalent to identity types based at [a], then the total space [sig R] is contractible. This is Lemma 5.8.2 (iii) => iv) *) +Definition contr_sigma_refl_rel {A : Type} + (a : A) (R : A -> Type) (r0 : R a) + (f : forall b, (a = b) <~> R b) + : Contr (sig R). +Proof. + rapply contr_equiv'. + 1: exact (equiv_functor_sigma_id f). + apply contr_basedpaths. +Defined. + +(** A pointed type family is an identity system if it satisfies the J-rule. *) +Class IsIdentitySystem {A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) + := + { IdentitySystem_ind (D : forall a : A, R a -> Type) (d : D a0 r0) (a : A) (r : R a) + : D a r; + + IdentitySystem_ind_beta (D : forall a : A, R a -> Type) (d : D a0 r0) + : IdentitySystem_ind D d a0 r0 = d + }. + +(** Given an identity system, transporting the point [r0] induces a fiber-wise equivalence between the based path type on [a0] and [R]. This is Theorem 5.8.2. (i) => (iii) from the Book. *) +Global Instance isequiv_transport_IsIdentitySystem {A : Type} {a0 : A} + (R : A -> Type) (r0 : R a0) `{!IsIdentitySystem _ r0} + (a : A) : IsEquiv (fun p : a0 = a => transport R p r0). +Proof. + pose (f := IdentitySystem_ind (fun a _ => a0 = a) (idpath _)). + pose (f_beta := IdentitySystem_ind_beta (fun a _ => a0 = a) (idpath _)). + snrapply isequiv_adjointify. + - exact (f a). + - exact ((IdentitySystem_ind + (fun (a' : A) (r' : R a') => transport R (f a' r') r0 = r') + (ap (fun x => transport R x r0) f_beta)) + a). + - by intros []. +Defined. + +Definition equiv_transport_IsIdentitySystem {A : Type} {a0 : A} + (R : A -> Type) (r0 : R a0) `{!IsIdentitySystem _ r0} + (a : A) : (a0 = a) <~> R a + := Build_Equiv _ _ (fun p => transport R p r0) _. + +(** I could use pointed maps, but this will introduce more dependencies. It might be wise to factor out this part of lemma 5.8.2. and relocate it, so that this file can depend on less, and add the full statement into contrib. Notice that we also need funext to make this work, so it isn't as nice as i) <=> iii) <=> iv) *) +Definition pfammap {A : Type} {a0 : A} (R S : A -> Type) (r0 : R a0) (s0 : S a0) : Type + := {f : forall a : A, R a -> S a & f a0 r0 = s0}. + +(** Personally, it does not spark joy that this little guy depends on function extensionality. I hope I'm wrong, otherwise we should cut him from the rest of the band. (i) => (ii) *) +Definition contr_pfammap_identitysystem `{Funext} {A : Type} {a0 : A} + (R : A -> Type) (r0 : R a0) `{!IsIdentitySystem R r0} (S : A -> Type) (s0 : S a0) + : Contr (pfammap R S r0 s0). +Proof. + pose (f := IdentitySystem_ind (fun a _ => S a) s0). + pose (f0 := IdentitySystem_ind_beta (fun a _ => S a) s0). + snrapply Build_Contr. + - exact (f ; f0). + - intro g; cbn. + pose (h := IdentitySystem_ind (fun (a : A) (r : R a) => f a r = pr1 g a r) (f0 @ (pr2 g)^)). + pose (h0 := IdentitySystem_ind_beta (fun (a : A) (r : R a) => f a r = pr1 g a r) (f0 @ (pr2 g)^)). + snrapply path_sigma. + + exact (path_forall _ _ (fun a => path_forall _ _ (h a))). + + cbn. + transport_path_forall_hammer. + lhs nrapply transport_paths_l. + nrapply moveR_Vp. + nrapply moveL_pM. + exact h0^. +Defined. + +(** (ii) => (iii). I literally hate this. *) +Global Instance equiv_path_contr_pfammap {A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) + (H : forall S : A -> Type, forall s0 : S a0, Contr (pfammap R S r0 s0)) + (a : A) : IsEquiv (fun p : a0 = a => transport R p r0). +Proof. + snrapply isequiv_adjointify. + - exact (pr1 (@center (pfammap _ _ _ _) (H (fun a => a0 = a) 1)) a). + - intro r. + pose (c := @center (pfammap _ _ _ _) (H R r0)). + srefine (_ @ _). + + exact (pr1 c a r). + + symmetry. + pose (inv := fun a r => transport R (pr1 (@center (pfammap _ _ _ _) (H (fun a => a0 = a) 1)) a r) r0). + pose (inv0 := (ap (fun x => transport R x r0) (pr2 (@center (pfammap _ _ _ _) (H (fun a => a0 = a) 1))))). + revert r; apply apD10. + revert a; apply apD10. + exact (ap pr1 (contr (@exist (forall a : A, R a -> R a) (fun f => f a0 r0 = r0) inv inv0))). + + revert r; apply apD10. + revert a; apply apD10. + exact (ap pr1 (contr (@exist (forall a : A, R a -> R a) (fun f => f a0 r0 = r0) (fun a r => r) 1))). + - intros []; cbn. + exact ((pr2 (@center (pfammap _ _ _ _) (H (fun a => a0 = a) 1)))). +Defined. \ No newline at end of file From 07b908ebe130d49a00ed852f7a5d8ca5ad4c6455 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Thomas=20Wilskow=20Thorbj=C3=B8rnsen?= Date: Thu, 21 Nov 2024 11:14:35 -0500 Subject: [PATCH 2/9] Missing new line --- theories/PathAny.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/PathAny.v b/theories/PathAny.v index d78d81a7ae2..903f788d99f 100644 --- a/theories/PathAny.v +++ b/theories/PathAny.v @@ -170,4 +170,4 @@ Proof. exact (ap pr1 (contr (@exist (forall a : A, R a -> R a) (fun f => f a0 r0 = r0) (fun a r => r) 1))). - intros []; cbn. exact ((pr2 (@center (pfammap _ _ _ _) (H (fun a => a0 = a) 1)))). -Defined. \ No newline at end of file +Defined. From 045f2f69b8f8a04d9081236bff0c2f1c66e64270 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Thomas=20Wilskow=20Thorbj=C3=B8rnsen?= <42666273+ThomatoTomato@users.noreply.github.com> Date: Thu, 21 Nov 2024 13:38:46 -0500 Subject: [PATCH 3/9] Update theories/PathAny.v Co-authored-by: Dan Christensen --- theories/PathAny.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/PathAny.v b/theories/PathAny.v index 903f788d99f..f077ba5e0e1 100644 --- a/theories/PathAny.v +++ b/theories/PathAny.v @@ -80,7 +80,7 @@ Ltac contr_sigsig a c := (** For examples of the use of this tactic, see for instance [Factorization] and [Idempotents]. *) -(** Given that some type family [R] is fiber-wise equivalent to identity types based at [a], then the total space [sig R] is contractible. This is Lemma 5.8.2 (iii) => iv) *) +(** Given that some type family [R] is fiber-wise equivalent to identity types based at [a], then the total space [sig R] is contractible. This is Theorem 5.8.2 (iii) => (iv). *) Definition contr_sigma_refl_rel {A : Type} (a : A) (R : A -> Type) (r0 : R a) (f : forall b, (a = b) <~> R b) From 8b27a22896c2d5cb71f50d0ec002a9a1c1b02f59 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Thomas=20Wilskow=20Thorbj=C3=B8rnsen?= <42666273+ThomatoTomato@users.noreply.github.com> Date: Thu, 21 Nov 2024 13:39:00 -0500 Subject: [PATCH 4/9] Update theories/PathAny.v Co-authored-by: Dan Christensen --- theories/PathAny.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/PathAny.v b/theories/PathAny.v index f077ba5e0e1..8d5c94f9be1 100644 --- a/theories/PathAny.v +++ b/theories/PathAny.v @@ -101,7 +101,7 @@ Class IsIdentitySystem {A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) : IdentitySystem_ind D d a0 r0 = d }. -(** Given an identity system, transporting the point [r0] induces a fiber-wise equivalence between the based path type on [a0] and [R]. This is Theorem 5.8.2. (i) => (iii) from the Book. *) +(** Given an identity system, transporting the point [r0] induces a fiber-wise equivalence between the based path type on [a0] and [R]. This is Theorem 5.8.2 (i) => (iii) from the Book. *) Global Instance isequiv_transport_IsIdentitySystem {A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) `{!IsIdentitySystem _ r0} (a : A) : IsEquiv (fun p : a0 = a => transport R p r0). From 6c4630febbf88b9611c30f3e0788191a1193d6d7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Thomas=20Wilskow=20Thorbj=C3=B8rnsen?= <42666273+ThomatoTomato@users.noreply.github.com> Date: Thu, 21 Nov 2024 13:39:06 -0500 Subject: [PATCH 5/9] Update theories/PathAny.v Co-authored-by: Dan Christensen --- theories/PathAny.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/PathAny.v b/theories/PathAny.v index 8d5c94f9be1..c8f5a5336b2 100644 --- a/theories/PathAny.v +++ b/theories/PathAny.v @@ -134,7 +134,7 @@ Proof. pose (f := IdentitySystem_ind (fun a _ => S a) s0). pose (f0 := IdentitySystem_ind_beta (fun a _ => S a) s0). snrapply Build_Contr. - - exact (f ; f0). + - exact (f; f0). - intro g; cbn. pose (h := IdentitySystem_ind (fun (a : A) (r : R a) => f a r = pr1 g a r) (f0 @ (pr2 g)^)). pose (h0 := IdentitySystem_ind_beta (fun (a : A) (r : R a) => f a r = pr1 g a r) (f0 @ (pr2 g)^)). From 716d22a437dd3f54f8602daf6d87c66513d34162 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Thomas=20Wilskow=20Thorbj=C3=B8rnsen?= Date: Fri, 22 Nov 2024 11:36:29 -0500 Subject: [PATCH 6/9] Weakening (ii) and style changes --- theories/PathAny.v | 62 ++++++++++++++++++++++------------------------ 1 file changed, 30 insertions(+), 32 deletions(-) diff --git a/theories/PathAny.v b/theories/PathAny.v index c8f5a5336b2..432b1df2ea8 100644 --- a/theories/PathAny.v +++ b/theories/PathAny.v @@ -106,13 +106,13 @@ Global Instance isequiv_transport_IsIdentitySystem {A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) `{!IsIdentitySystem _ r0} (a : A) : IsEquiv (fun p : a0 = a => transport R p r0). Proof. - pose (f := IdentitySystem_ind (fun a _ => a0 = a) (idpath _)). - pose (f_beta := IdentitySystem_ind_beta (fun a _ => a0 = a) (idpath _)). + pose (to_paths := IdentitySystem_ind (fun a _ => a0 = a) (idpath _)). + pose (to_paths_beta := IdentitySystem_ind_beta (fun a _ => a0 = a) (idpath _)). snrapply isequiv_adjointify. - - exact (f a). + - exact (to_paths a). - exact ((IdentitySystem_ind - (fun (a' : A) (r' : R a') => transport R (f a' r') r0 = r') - (ap (fun x => transport R x r0) f_beta)) + (fun (a' : A) (r' : R a') => transport R (to_paths a' r') r0 = r') + (ap (fun x => transport R x r0) to_paths_beta)) a). - by intros []. Defined. @@ -123,45 +123,43 @@ Definition equiv_transport_IsIdentitySystem {A : Type} {a0 : A} := Build_Equiv _ _ (fun p => transport R p r0) _. (** I could use pointed maps, but this will introduce more dependencies. It might be wise to factor out this part of lemma 5.8.2. and relocate it, so that this file can depend on less, and add the full statement into contrib. Notice that we also need funext to make this work, so it isn't as nice as i) <=> iii) <=> iv) *) -Definition pfammap {A : Type} {a0 : A} (R S : A -> Type) (r0 : R a0) (s0 : S a0) : Type +Definition pfamMap {A : Type} {a0 : A} + (R S : A -> Type) (r0 : R a0) (s0 : S a0) : Type := {f : forall a : A, R a -> S a & f a0 r0 = s0}. -(** Personally, it does not spark joy that this little guy depends on function extensionality. I hope I'm wrong, otherwise we should cut him from the rest of the band. (i) => (ii) *) -Definition contr_pfammap_identitysystem `{Funext} {A : Type} {a0 : A} - (R : A -> Type) (r0 : R a0) `{!IsIdentitySystem R r0} (S : A -> Type) (s0 : S a0) - : Contr (pfammap R S r0 s0). +Definition path_pfamMap {A : Type} {a0 : A} + {R S : A -> Type} {r0 : R a0} {s0 : S a0} + (f g : pfamMap R S r0 s0) : Type + := { p : forall a : A, pr1 f a == pr1 g a & p a0 r0 = pr2 f @ (pr2 g)^}. + +(** A weak form of (i) => (ii) *) +Definition homocontr_pfamMap_identitysystem {A : Type} {a0 : A} + (R : A -> Type) (r0 : R a0) `{!IsIdentitySystem R r0} + (S : A -> Type) (s0 : S a0) + : exists f : pfamMap R S r0 s0, forall g, path_pfamMap f g. Proof. - pose (f := IdentitySystem_ind (fun a _ => S a) s0). - pose (f0 := IdentitySystem_ind_beta (fun a _ => S a) s0). - snrapply Build_Contr. - - exact (f; f0). - - intro g; cbn. - pose (h := IdentitySystem_ind (fun (a : A) (r : R a) => f a r = pr1 g a r) (f0 @ (pr2 g)^)). - pose (h0 := IdentitySystem_ind_beta (fun (a : A) (r : R a) => f a r = pr1 g a r) (f0 @ (pr2 g)^)). - snrapply path_sigma. - + exact (path_forall _ _ (fun a => path_forall _ _ (h a))). - + cbn. - transport_path_forall_hammer. - lhs nrapply transport_paths_l. - nrapply moveR_Vp. - nrapply moveL_pM. - exact h0^. + pose (to_S := IdentitySystem_ind (fun a _ => S a) s0). + pose proof (to_S_beta := IdentitySystem_ind_beta (fun a _ => S a) s0). + snrefine ((to_S; to_S_beta); _). + intro g; cbn. + exists (IdentitySystem_ind (fun a r => to_S a r = pr1 g a r) (to_S_beta @ (pr2 g)^)). + snrapply IdentitySystem_ind_beta. Defined. (** (ii) => (iii). I literally hate this. *) -Global Instance equiv_path_contr_pfammap {A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) - (H : forall S : A -> Type, forall s0 : S a0, Contr (pfammap R S r0 s0)) +Global Instance equiv_path_contr_pfamMap {A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) + (H : forall S : A -> Type, forall s0 : S a0, Contr (pfamMap R S r0 s0)) (a : A) : IsEquiv (fun p : a0 = a => transport R p r0). Proof. snrapply isequiv_adjointify. - - exact (pr1 (@center (pfammap _ _ _ _) (H (fun a => a0 = a) 1)) a). + - exact (pr1 (@center (pfamMap _ _ _ _) (H (fun a => a0 = a) 1)) a). - intro r. - pose (c := @center (pfammap _ _ _ _) (H R r0)). + pose (c := @center (pfamMap _ _ _ _) (H R r0)). srefine (_ @ _). + exact (pr1 c a r). + symmetry. - pose (inv := fun a r => transport R (pr1 (@center (pfammap _ _ _ _) (H (fun a => a0 = a) 1)) a r) r0). - pose (inv0 := (ap (fun x => transport R x r0) (pr2 (@center (pfammap _ _ _ _) (H (fun a => a0 = a) 1))))). + pose (inv := fun a r => transport R (pr1 (@center (pfamMap _ _ _ _) (H (fun a => a0 = a) 1)) a r) r0). + pose (inv0 := (ap (fun x => transport R x r0) (pr2 (@center (pfamMap _ _ _ _) (H (fun a => a0 = a) 1))))). revert r; apply apD10. revert a; apply apD10. exact (ap pr1 (contr (@exist (forall a : A, R a -> R a) (fun f => f a0 r0 = r0) inv inv0))). @@ -169,5 +167,5 @@ Proof. revert a; apply apD10. exact (ap pr1 (contr (@exist (forall a : A, R a -> R a) (fun f => f a0 r0 = r0) (fun a r => r) 1))). - intros []; cbn. - exact ((pr2 (@center (pfammap _ _ _ _) (H (fun a => a0 = a) 1)))). + exact ((pr2 (@center (pfamMap _ _ _ _) (H (fun a => a0 = a) 1)))). Defined. From 8e7e6f8b3f27dc8a9c13cb67e0f7c1d7b04930dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Thomas=20Wilskow=20Thorbj=C3=B8rnsen?= Date: Fri, 22 Nov 2024 12:39:14 -0500 Subject: [PATCH 7/9] (ii)' => (iii) --- theories/PathAny.v | 37 ++++++++++++++++--------------------- 1 file changed, 16 insertions(+), 21 deletions(-) diff --git a/theories/PathAny.v b/theories/PathAny.v index 432b1df2ea8..8ffcd524110 100644 --- a/theories/PathAny.v +++ b/theories/PathAny.v @@ -94,8 +94,8 @@ Defined. (** A pointed type family is an identity system if it satisfies the J-rule. *) Class IsIdentitySystem {A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) := - { IdentitySystem_ind (D : forall a : A, R a -> Type) (d : D a0 r0) (a : A) (r : R a) - : D a r; + { IdentitySystem_ind (D : forall a : A, R a -> Type) (d : D a0 r0) + (a : A) (r : R a) : D a r; IdentitySystem_ind_beta (D : forall a : A, R a -> Type) (d : D a0 r0) : IdentitySystem_ind D d a0 r0 = d @@ -146,26 +146,21 @@ Proof. snrapply IdentitySystem_ind_beta. Defined. -(** (ii) => (iii). I literally hate this. *) -Global Instance equiv_path_contr_pfamMap {A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) - (H : forall S : A -> Type, forall s0 : S a0, Contr (pfamMap R S r0 s0)) +(** A strong form of (ii) => (iii) *) +Definition equiv_path_homocontr_pfamMap {A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) + (H : forall S : A -> Type, forall s0 : S a0, exists f : pfamMap R S r0 s0, forall g, path_pfamMap f g) (a : A) : IsEquiv (fun p : a0 = a => transport R p r0). Proof. - snrapply isequiv_adjointify. - - exact (pr1 (@center (pfamMap _ _ _ _) (H (fun a => a0 = a) 1)) a). + pose (inv (a : A) := (pr1 o pr1) (H (fun a => a0 = a) 1) a). + pose proof (inv_beta := (pr2 o pr1) (H (fun a => a0 = a) 1)); cbn in inv_beta. + snrapply (isequiv_adjointify _ (inv a)); cbn. - intro r. - pose (c := @center (pfamMap _ _ _ _) (H R r0)). - srefine (_ @ _). - + exact (pr1 c a r). + snrefine (_ @ _). + + exact ((pr1 o pr1) (H R r0) a r). + symmetry. - pose (inv := fun a r => transport R (pr1 (@center (pfamMap _ _ _ _) (H (fun a => a0 = a) 1)) a r) r0). - pose (inv0 := (ap (fun x => transport R x r0) (pr2 (@center (pfamMap _ _ _ _) (H (fun a => a0 = a) 1))))). - revert r; apply apD10. - revert a; apply apD10. - exact (ap pr1 (contr (@exist (forall a : A, R a -> R a) (fun f => f a0 r0 = r0) inv inv0))). - + revert r; apply apD10. - revert a; apply apD10. - exact (ap pr1 (contr (@exist (forall a : A, R a -> R a) (fun f => f a0 r0 = r0) (fun a r => r) 1))). - - intros []; cbn. - exact ((pr2 (@center (pfamMap _ _ _ _) (H (fun a => a0 = a) 1)))). -Defined. + exact ((pr1 (pr2 (H R r0) (fun a r => transport R (inv a r) r0; + ((ap (fun x => transport R x r0) inv_beta))))) a r). + + exact ((pr1 (pr2 (H R r0) (fun a r => r; + (idpath r0)))) a r). + - by intros []. +Defined. \ No newline at end of file From 5f2eb2435e6f12397c58ffbab3a6e024c2c57fa5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Thomas=20Wilskow=20Thorbj=C3=B8rnsen?= Date: Fri, 22 Nov 2024 12:46:39 -0500 Subject: [PATCH 8/9] Removed WIP --- contrib/HoTTBook.v | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/contrib/HoTTBook.v b/contrib/HoTTBook.v index 18cadbd7cd6..736c8330886 100644 --- a/contrib/HoTTBook.v +++ b/contrib/HoTTBook.v @@ -769,20 +769,8 @@ Definition Book_4_9_5 := @HoTT.Metatheory.FunextVarieties.WeakFunext_implies_Fun (* ================================================== thm:identity-systems *) (** Theorem 5.8.2 *) -Definition Book_5_8_2_i_implies_iii := @HoTT.PathAny.equiv_transport_IsIdentitySystem. -Definition Book_5_8_2_iii_implies_i {A} {a0 : A} {X : A -> Type} (x0 : X a0) - (e : forall (a : A), IsEquiv (fun p : a0 = a => transport X p x0)) - (P : forall (b : A), X b -> Type) - (r : P a0 x0) - := @HoTT.Basics.Equivalences.equiv_path_ind A a0 X - (fun a => @Build_Equiv _ _ _ (e a)) P r. - -Definition Book_5_8_2_iii_implies_iv := @HoTT.PathAny.contr_sigma_refl_rel. Definition Book_5_8_2_iv_implies_iii := @HoTT.PathAny.equiv_path_from_contr. -Definition Book_5_8_2_i_implies_ii := @HoTT.PathAny.contr_pfammap_identitysystem. -Definition Book_5_8_2_ii_implies_iii := @HoTT.PathAny.equiv_path_contr_pfammap. - (* ================================================== thm:ML-identity-systems *) (** Theorem 5.8.4 *) From 952cc85146a854ec4351cbe2f0e504a242088b36 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Thomas=20Wilskow=20Thorbj=C3=B8rnsen?= Date: Fri, 22 Nov 2024 17:52:02 -0500 Subject: [PATCH 9/9] Theorem 5.8.2 --- contrib/HoTTBook.v | 2 +- theories/PathAny.v | 107 ++++++++++++++++++++++++++++----------------- 2 files changed, 68 insertions(+), 41 deletions(-) diff --git a/contrib/HoTTBook.v b/contrib/HoTTBook.v index 736c8330886..1a13b7a0799 100644 --- a/contrib/HoTTBook.v +++ b/contrib/HoTTBook.v @@ -769,7 +769,7 @@ Definition Book_4_9_5 := @HoTT.Metatheory.FunextVarieties.WeakFunext_implies_Fun (* ================================================== thm:identity-systems *) (** Theorem 5.8.2 *) -Definition Book_5_8_2_iv_implies_iii := @HoTT.PathAny.equiv_path_from_contr. +Definition Book_5_8_2 := @HoTT.PathAny.FundamentalThmIdentitySystems. (* ================================================== thm:ML-identity-systems *) (** Theorem 5.8.4 *) diff --git a/theories/PathAny.v b/theories/PathAny.v index 8ffcd524110..9a0c0623121 100644 --- a/theories/PathAny.v +++ b/theories/PathAny.v @@ -80,7 +80,7 @@ Ltac contr_sigsig a c := (** For examples of the use of this tactic, see for instance [Factorization] and [Idempotents]. *) -(** Given that some type family [R] is fiber-wise equivalent to identity types based at [a], then the total space [sig R] is contractible. This is Theorem 5.8.2 (iii) => (iv). *) +(** Given that some type family [R] is fiber-wise equivalent to identity types based at [a], then the total space [sig R] is contractible. This is part of Theorem 5.8.2, (iii) implies (iv). *) Definition contr_sigma_refl_rel {A : Type} (a : A) (R : A -> Type) (r0 : R a) (f : forall b, (a = b) <~> R b) @@ -91,48 +91,27 @@ Proof. apply contr_basedpaths. Defined. -(** A pointed type family is an identity system if it satisfies the J-rule. *) +(** There are also some additional properties that we can be use to characterize identity types. A pointed type family is an identity system if it satisfies the J-rule. *) Class IsIdentitySystem {A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) := - { IdentitySystem_ind (D : forall a : A, R a -> Type) (d : D a0 r0) - (a : A) (r : R a) : D a r; - + { IdentitySystem_ind (D : forall a : A, R a -> Type) (d : D a0 r0) (a : A) (r : R a) + : D a r; IdentitySystem_ind_beta (D : forall a : A, R a -> Type) (d : D a0 r0) : IdentitySystem_ind D d a0 r0 = d }. -(** Given an identity system, transporting the point [r0] induces a fiber-wise equivalence between the based path type on [a0] and [R]. This is Theorem 5.8.2 (i) => (iii) from the Book. *) -Global Instance isequiv_transport_IsIdentitySystem {A : Type} {a0 : A} - (R : A -> Type) (r0 : R a0) `{!IsIdentitySystem _ r0} - (a : A) : IsEquiv (fun p : a0 = a => transport R p r0). -Proof. - pose (to_paths := IdentitySystem_ind (fun a _ => a0 = a) (idpath _)). - pose (to_paths_beta := IdentitySystem_ind_beta (fun a _ => a0 = a) (idpath _)). - snrapply isequiv_adjointify. - - exact (to_paths a). - - exact ((IdentitySystem_ind - (fun (a' : A) (r' : R a') => transport R (to_paths a' r') r0 = r') - (ap (fun x => transport R x r0) to_paths_beta)) - a). - - by intros []. -Defined. - -Definition equiv_transport_IsIdentitySystem {A : Type} {a0 : A} - (R : A -> Type) (r0 : R a0) `{!IsIdentitySystem _ r0} - (a : A) : (a0 = a) <~> R a - := Build_Equiv _ _ (fun p => transport R p r0) _. - -(** I could use pointed maps, but this will introduce more dependencies. It might be wise to factor out this part of lemma 5.8.2. and relocate it, so that this file can depend on less, and add the full statement into contrib. Notice that we also need funext to make this work, so it isn't as nice as i) <=> iii) <=> iv) *) +(** The mapping space between two pointed type families over the same base point, is a family of maps that preserves the basepoint. *) Definition pfamMap {A : Type} {a0 : A} (R S : A -> Type) (r0 : R a0) (s0 : S a0) : Type := {f : forall a : A, R a -> S a & f a0 r0 = s0}. +(** We can also consider pointed homotopies between maps of pointed type families. *) Definition path_pfamMap {A : Type} {a0 : A} {R S : A -> Type} {r0 : R a0} {s0 : S a0} (f g : pfamMap R S r0 s0) : Type := { p : forall a : A, pr1 f a == pr1 g a & p a0 r0 = pr2 f @ (pr2 g)^}. -(** A weak form of (i) => (ii) *) +(** Given that a pointed type family [R], [r0] is an identity system, then the mapping space of pointed type families starting at [R] is homotopy contractible. This is a weak form of Theorem 5.8.2, (i) implies (ii). *) Definition homocontr_pfamMap_identitysystem {A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) `{!IsIdentitySystem R r0} (S : A -> Type) (s0 : S a0) @@ -141,26 +120,74 @@ Proof. pose (to_S := IdentitySystem_ind (fun a _ => S a) s0). pose proof (to_S_beta := IdentitySystem_ind_beta (fun a _ => S a) s0). snrefine ((to_S; to_S_beta); _). - intro g; cbn. - exists (IdentitySystem_ind (fun a r => to_S a r = pr1 g a r) (to_S_beta @ (pr2 g)^)). + intro g. + exists (IdentitySystem_ind (fun a r => to_S a r = pr1 g a r) + (to_S_beta @ (pr2 g)^)). snrapply IdentitySystem_ind_beta. Defined. -(** A strong form of (ii) => (iii) *) +(** If a pointed type family [R], [r0] has homotopy contractible mapping spaces as in the sense above, then [fun p => transport R p r0] is a fiber-wise equivalence. This is a strong form of Theorem 5.8.2, (ii) implies (iii). *) Definition equiv_path_homocontr_pfamMap {A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) - (H : forall S : A -> Type, forall s0 : S a0, exists f : pfamMap R S r0 s0, forall g, path_pfamMap f g) - (a : A) : IsEquiv (fun p : a0 = a => transport R p r0). + (H : forall S : A -> Type, forall s0 : S a0, exists f : pfamMap R S r0 s0, forall g, path_pfamMap f g) (a : A) + : IsEquiv (fun p : a0 = a => transport R p r0). Proof. pose (inv (a : A) := (pr1 o pr1) (H (fun a => a0 = a) 1) a). - pose proof (inv_beta := (pr2 o pr1) (H (fun a => a0 = a) 1)); cbn in inv_beta. + pose proof (inv_beta := (pr2 o pr1) (H (fun a => a0 = a) 1)); + cbn in inv_beta. snrapply (isequiv_adjointify _ (inv a)); cbn. - intro r. snrefine (_ @ _). + exact ((pr1 o pr1) (H R r0) a r). - + symmetry. - exact ((pr1 (pr2 (H R r0) (fun a r => transport R (inv a r) r0; - ((ap (fun x => transport R x r0) inv_beta))))) a r). - + exact ((pr1 (pr2 (H R r0) (fun a r => r; - (idpath r0)))) a r). + + exact ((pr1 (pr2 (H R r0) + (fun a r => transport R (inv a r) r0; + ((ap (fun x => transport R x r0) inv_beta))))) a r)^. + + exact ((pr1 (pr2 (H R r0) (fun a r => r; (idpath r0)))) a r). - by intros []. -Defined. \ No newline at end of file +Defined. + +(** For any pointed type family [R], [r0] such that the total space of [R] is contractible, then [R], [r0] is an identity system. This is Theorem 5.8.2, (iv) implies (i). *) +Definition IsIdentitySystem_contr_sigma {A : Type} {a0 : A} (R : A -> Type) + (r0 : R a0) {C : Contr (sig R)} + : IsIdentitySystem R r0. +Proof. + snrapply Build_IsIdentitySystem. + - intros D d0 a r. + exact (transport + (fun ar : sig R => D (pr1 ar) (pr2 ar)) + ((@contr _ C (a0; r0))^ @ @contr _ C (a; r)) d0). + - intros D d0; cbn. + by lhs nrapply (ap (fun x => transport _ x _) (concat_Vp _)). +Defined. + +(** The fundamental theorem of identity systems tells us that these four different properties are logically equivalent. *) +Definition FundamentalThmIdentitySystems {A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) + : (IsIdentitySystem R r0 -> forall S : A -> Type, forall s0 : S a0, exists f : pfamMap R S r0 s0, forall g, path_pfamMap f g) + * ((forall S : A -> Type, forall s0 : S a0, + exists f : pfamMap R S r0 s0, forall g, path_pfamMap f g) + -> forall a : A, IsEquiv (fun p : a0 = a => transport R p r0)) + * ((forall a : A, IsEquiv (fun p : a0 = a => transport R p r0)) + -> Contr (sig R)) + * (Contr (sig R) -> IsIdentitySystem R r0). +Proof. + repeat split. + - nrapply homocontr_pfamMap_identitysystem. + - nrapply equiv_path_homocontr_pfamMap. + - intros e_transport. + exact (contr_sigma_refl_rel a0 R r0 + (fun a => @Build_Equiv _ _ _ (e_transport a))). + - nrapply IsIdentitySystem_contr_sigma. +Defined. + +(** It is useful to have some composites of the above. Given an identity system, transporting the point [r0] induces a fiber-wise equivalence between the based path type on [a0] and [R]. This is Theorem 5.8.2 (i) implies (iii) from the Book. *) +Global Instance isequiv_transport_IsIdentitySystem {A : Type} {a0 : A} + (R : A -> Type) (r0 : R a0) `{!IsIdentitySystem _ r0} (a : A) + : IsEquiv (fun p : a0 = a => transport R p r0). +Proof. + nrapply equiv_path_homocontr_pfamMap. + by nrapply homocontr_pfamMap_identitysystem. +Defined. + +Definition equiv_transport_IsIdentitySystem {A : Type} {a0 : A} + (R : A -> Type) (r0 : R a0) `{!IsIdentitySystem _ r0} (a : A) + : (a0 = a) <~> R a + := Build_Equiv _ _ (fun p => transport R p r0) _.