From ab0380bab7067257a344827c01f3efdfb4b42fd6 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Mon, 8 Apr 2024 01:17:06 +0100
Subject: [PATCH] I-indexed coproducts in pType

Signed-off-by: Ali Caglayan <alizter@gmail.com>

<!-- ps-id: 1fdec980-f07a-41c8-901d-044d7f50051e -->
---
 theories/Homotopy/Wedge.v | 45 +++++++++++++++++++++++++++++++++------
 1 file changed, 39 insertions(+), 6 deletions(-)

diff --git a/theories/Homotopy/Wedge.v b/theories/Homotopy/Wedge.v
index b0636683096..094899fe458 100644
--- a/theories/Homotopy/Wedge.v
+++ b/theories/Homotopy/Wedge.v
@@ -194,14 +194,14 @@ Proof.
     exact pt.
 Defined.
 
+Definition fwedge_in' (I : Type) (X : I -> pType)
+  : forall i, X i $-> FamilyWedge I X
+  := fun i => Build_pMap _ _ (fun x => pushl (i; x)) (pglue pt).
+
 (** 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.
+  : psigma (pointed_fam X) $-> FamilyWedge I X
+  := Build_pMap _ _ pushl (pglue pt).
 
 (** Recursion principle for the wedge of an indexed family of pointed types. *)
 Definition fwedge_rec (I : Type) (X : I -> pType) (Z : pType)
@@ -230,6 +230,39 @@ Proof.
   - exact pconst.
 Defined.
 
+Global Instance hascoproducts_ptype (I : Type) : HasCoproducts I pType.
+Proof.
+  intros X.
+  snrapply Build_Coproduct.
+  - exact (FamilyWedge I X).
+  - exact (fwedge_in' I X).
+  - exact (fwedge_rec I X).
+  - intros Z f i.
+    snrapply Build_pHomotopy.
+    1: reflexivity.
+    simpl.
+    apply moveL_pV.
+    apply equiv_1p_q1.
+    symmetry.
+    exact (Pushout_rec_beta_pglue Z _ (unit_name pt) (fun i => point_eq (f i)) _).
+  - intros Z f g h.
+    snrapply Build_pHomotopy.
+    + snrapply Pushout_ind.
+      * intros [i x].
+        nrapply h.
+      * intros [].
+        exact (point_eq _ @ (point_eq _)^).
+      * intros i.
+        nrapply transport_paths_FlFr'.
+        lhs nrapply concat_p_pp.
+        apply moveR_pV.
+        rhs nrapply concat_pp_p.
+        apply moveL_pM.
+        symmetry.
+        exact (dpoint_eq (h i)).
+    + reflexivity.
+Defined.
+
 (** ** The pinch map on the suspension *)
 
 (** Given a suspension, there is a natural map from the suspension to the wedge of the suspension with itself. This is known as the pinch map.