From a42516d39c8e2c5e6144cd186d589d79ecd2d37b Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 24 Jan 2024 17:43:21 +0000 Subject: [PATCH 1/3] Wedge of a family of pType Signed-off-by: Ali Caglayan --- theories/Homotopy/Wedge.v | 67 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 65 insertions(+), 2 deletions(-) diff --git a/theories/Homotopy/Wedge.v b/theories/Homotopy/Wedge.v index 73280acedb6..9ed19c3ffc6 100644 --- a/theories/Homotopy/Wedge.v +++ b/theories/Homotopy/Wedge.v @@ -1,4 +1,4 @@ -Require Import Basics Types.Paths. +Require Import Basics Types. Require Import Pointed.Core. Require Import Colimits.Pushout. Require Import WildCat. @@ -100,4 +100,67 @@ Proof. by pelim f g. - intros Z f g p q. by apply wedge_up. -Defined. \ No newline at end of file +Defined. + +(** Wedge of an indexed family of pointed types *) + +(** Note that the index type is not necesserily pointed. An empty wedge is the unit type which is the zero object in the category of pointed types. *) +Definition FamilyWedge (I : Type) (X : I -> pType) : pType. +Proof. + srefine ([_, _]). + - srefine (Pushout (A := sig (fun _ : I => pUnit)) (B := sig X) (C := pUnit) _ _). + + snrapply functor_sigma. + 1: exact idmap. + intros i. + exact (fun _ => pt). + + exact (fun _ => pt). + - apply pushr. + exact pt. +Defined. + +(** We can define an inclusion map if the index set is non-empty. In the empty case the wedge should be equivalent to the unit type anyway. *) +Definition fwedge_in (I : pType) (X : I -> pType) + : psigma (pointed_fam X) $-> FamilyWedge I X. +Proof. + snrapply Build_pMap. + - exact pushl. + - exact (pglue (pt; pt)). +Defined. + +(** Recursion principle for the wedge of an indexed family of pointed types. *) +Definition fwedge_rec (I : Type) (X : I -> pType) (Z : pType) + (f : forall i, X i $-> Z) + : FamilyWedge I X $-> Z. +Proof. + snrapply Build_pMap. + - snrapply Pushout_rec. + + apply (sig_rec _ _ _ f). + + exact pconst. + + intros [i ]. + exact (point_eq (f i)). + - exact idpath. +Defined. + +(** Wedge inclusions into the product can be defined if the indexing type has decidable paths. This is because we need to choose which factor a given wedge should land. This makes it somewhat awkward to define an indexed smash product. + +TODO: is this strictly necessary or are their weaker assumptions we can use? Can we remove funext? *) +Definition fwedge_incl `{Funext} (I : Type) `(DecidablePaths I) (X : I -> pType) + : FamilyWedge I X $-> pproduct X. +Proof. + snrapply Build_pMap. + - snrapply Pushout_rec. + + intros [i x] a. + destruct (dec_paths i a). + * destruct p. + exact x. + * exact pt. + + exact (fun _ => pt). + + intros [i ]. + simpl. + apply path_forall. + intros a. + destruct (dec_paths i a). + * by destruct p. + * reflexivity. + - exact idpath. +Defined. From c80a3a638fa88113c6b595a36808f9fd23206cef Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 25 Jan 2024 15:05:57 +0000 Subject: [PATCH 2/3] address review comments for wedge Signed-off-by: Ali Caglayan --- theories/Homotopy/Wedge.v | 33 +++++++++++---------------------- theories/Pointed/Core.v | 12 ++++++++++++ 2 files changed, 23 insertions(+), 22 deletions(-) diff --git a/theories/Homotopy/Wedge.v b/theories/Homotopy/Wedge.v index 9ed19c3ffc6..1a2d28a53f8 100644 --- a/theories/Homotopy/Wedge.v +++ b/theories/Homotopy/Wedge.v @@ -107,7 +107,7 @@ Defined. (** Note that the index type is not necesserily pointed. An empty wedge is the unit type which is the zero object in the category of pointed types. *) Definition FamilyWedge (I : Type) (X : I -> pType) : pType. Proof. - srefine ([_, _]). + snrapply Build_pType. - srefine (Pushout (A := sig (fun _ : I => pUnit)) (B := sig X) (C := pUnit) _ _). + snrapply functor_sigma. 1: exact idmap. @@ -118,7 +118,7 @@ Proof. exact pt. Defined. -(** We can define an inclusion map if the index set is non-empty. In the empty case the wedge should be equivalent to the unit type anyway. *) +(** We have an inclusion map [pushl : sig X -> FamilyWedge X]. When [I] is pointed, so is [sig X], and then this inclusion map is pointed. *) Definition fwedge_in (I : pType) (X : I -> pType) : psigma (pointed_fam X) $-> FamilyWedge I X. Proof. @@ -136,31 +136,20 @@ Proof. - snrapply Pushout_rec. + apply (sig_rec _ _ _ f). + exact pconst. - + intros [i ]. + + intros [i ?]. exact (point_eq (f i)). - exact idpath. Defined. -(** Wedge inclusions into the product can be defined if the indexing type has decidable paths. This is because we need to choose which factor a given wedge should land. This makes it somewhat awkward to define an indexed smash product. - -TODO: is this strictly necessary or are their weaker assumptions we can use? Can we remove funext? *) +(** Wedge inclusions into the product can be defined if the indexing type has decidable paths. This is because we need to choose which factor a given wedge should land. This makes it somewhat awkward to work with, however in practice we typically only care about decidable index sets. *) Definition fwedge_incl `{Funext} (I : Type) `(DecidablePaths I) (X : I -> pType) : FamilyWedge I X $-> pproduct X. Proof. - snrapply Build_pMap. - - snrapply Pushout_rec. - + intros [i x] a. - destruct (dec_paths i a). - * destruct p. - exact x. - * exact pt. - + exact (fun _ => pt). - + intros [i ]. - simpl. - apply path_forall. - intros a. - destruct (dec_paths i a). - * by destruct p. - * reflexivity. - - exact idpath. + snrapply fwedge_rec. + intro i. + snrapply pproduct_corec. + intro a. + destruct (dec_paths i a). + - destruct p; exact pmap_idmap. + - exact pconst. Defined. diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v index 23664df8729..91467b85049 100644 --- a/theories/Pointed/Core.v +++ b/theories/Pointed/Core.v @@ -158,6 +158,18 @@ Definition psigma {A : pType} (P : pFam A) : pType Definition pproduct {A : Type} (F : A -> pType) : pType := [forall (a : A), pointed_type (F a), ispointed_type o F]. +Definition pproduct_corec `{Funext} {A : Type} (F : A -> pType) + (X : pType) (f : forall a, X ->* F a) + : X ->* pproduct F. +Proof. + snrapply Build_pMap. + - intros x a. + exact (f a x). + - cbn. + funext a. + apply point_eq. +Defined. + (** The following tactics often allow us to "pretend" that pointed maps and homotopies preserve basepoints strictly. *) (** First a version with no rewrites, which leaves some cleanup to be done but which can be used in transparent proofs. *) From 1d3ee90f189639181f531ce7234e1a6566ef59fc Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 25 Jan 2024 15:33:26 +0000 Subject: [PATCH 3/3] simplify definition of indexed wedge We don't have to convert the indexing type into a pointed type, it already is a type! Signed-off-by: Ali Caglayan --- theories/Homotopy/Wedge.v | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/theories/Homotopy/Wedge.v b/theories/Homotopy/Wedge.v index 1a2d28a53f8..346a23ed9db 100644 --- a/theories/Homotopy/Wedge.v +++ b/theories/Homotopy/Wedge.v @@ -108,11 +108,8 @@ Defined. Definition FamilyWedge (I : Type) (X : I -> pType) : pType. Proof. snrapply Build_pType. - - srefine (Pushout (A := sig (fun _ : I => pUnit)) (B := sig X) (C := pUnit) _ _). - + snrapply functor_sigma. - 1: exact idmap. - intros i. - exact (fun _ => pt). + - srefine (Pushout (A := I) (B := sig X) (C := pUnit) _ _). + + exact (fun i => (i; pt)). + exact (fun _ => pt). - apply pushr. exact pt. @@ -124,7 +121,7 @@ Definition fwedge_in (I : pType) (X : I -> pType) Proof. snrapply Build_pMap. - exact pushl. - - exact (pglue (pt; pt)). + - exact (pglue pt). Defined. (** Recursion principle for the wedge of an indexed family of pointed types. *) @@ -136,7 +133,7 @@ Proof. - snrapply Pushout_rec. + apply (sig_rec _ _ _ f). + exact pconst. - + intros [i ?]. + + intros i. exact (point_eq (f i)). - exact idpath. Defined.