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

<!-- ps-id: 1fdec980-f07a-41c8-901d-044d7f50051e -->

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 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..ce4a574f4ed 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 hasallcoproducts_ptype : HasAllCoproducts pType.
+Proof.
+  intros I 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.

From cff20adfaf8792cc83aed1e48bc0a2bc8fa44fe0 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Sat, 13 Apr 2024 15:13:16 +0100
Subject: [PATCH 2/2] Apply suggestions from code review

Co-authored-by: Dan Christensen <jdc+github@uwo.ca>
---
 theories/Homotopy/Wedge.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Homotopy/Wedge.v b/theories/Homotopy/Wedge.v
index ce4a574f4ed..ab09323d248 100644
--- a/theories/Homotopy/Wedge.v
+++ b/theories/Homotopy/Wedge.v
@@ -196,7 +196,7 @@ 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).
+  := fun i => Build_pMap _ _ (fun x => pushl (i; x)) (pglue i).
 
 (** 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)
@@ -252,7 +252,7 @@ Proof.
         nrapply h.
       * intros [].
         exact (point_eq _ @ (point_eq _)^).
-      * intros i.
+      * intros i; cbn.
         nrapply transport_paths_FlFr'.
         lhs nrapply concat_p_pp.
         apply moveR_pV.