Wedge of a family of pType

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,53 @@ Proof.
     by pelim f g.
   - intros Z f g p q.
     by apply wedge_up.
-Defined.
+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.
+  snrapply Build_pType.
+  - srefine (Pushout (A := I) (B := sig X) (C := pUnit) _ _).
+    + exact (fun i => (i; pt)).
+    + exact (fun _ => pt).
+  - apply pushr.
+    exact pt.
+Defined.
+
+(** 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.
+  snrapply Build_pMap.
+  - exact pushl.
+  - exact (pglue 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 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 fwedge_rec.
+  intro i.
+  snrapply pproduct_corec.
+  intro a.
+  destruct (dec_paths i a).
+  - destruct p; exact pmap_idmap.
+  - exact pconst.
+Defined.

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. *)