wedge projections

theories/Homotopy/Wedge.v

@@ -41,9 +41,14 @@ Proof.
   - exact (point_eq f).
 Defined.
 
-Definition wedge_incl {X Y : pType} : X \/ Y -> X * Y :=
- Pushout_rec _ (fun x => (x, point Y)) (fun y => (point X, y)) 
-  (fun _ : Unit => idpath).
+Definition wedge_pr1 {X Y : pType} : X \/ Y $-> X
+  := wedge_rec pmap_idmap pconst.
+
+Definition wedge_pr2 {X Y : pType} : X \/ Y $-> Y
+  := wedge_rec pconst pmap_idmap.
+
+Definition wedge_incl {X Y : pType} : X \/ Y -> X * Y
+  := pprod_corec _ wedge_pr1 wedge_pr2.
 
 (** 1-universal property of wedge. *)
 (** TODO: remove rewrites. For some reason pelim is not able to immediately abstract the goal so some shuffling around is necessery. *)

theories/Pointed/Core.v

@@ -91,13 +91,6 @@ Definition pmap_compose {A B C : pType} (g : B ->* C) (f : A ->* B)
 
 Infix "o*" := pmap_compose : pointed_scope.
 
-(** The projections from a pointed product are pointed maps. *)
-Definition pfst {A B : pType} : A * B ->* A
-  := Build_pMap (A * B) A fst idpath.
-
-Definition psnd {A B : pType} : A * B ->* B
-  := Build_pMap (A * B) B snd idpath.
-
 (** ** Pointed homotopies *)
 
 (** A pointed homotopy is a homotopy with a proof that the presevation paths agree. We define it instead as a special case of a [pForall]. This means that we can define pointed homotopies between pointed homotopies. *)
@@ -154,6 +147,8 @@ Definition pequiv_pmap_idmap {A} : A <~>* A
 Definition psigma {A : pType} (P : pFam A) : pType
   := [sig P, (point A; dpoint P)].
 
+(** *** Pointed products *)
+
 (** Pointed pi types; note that the domain is not pointed *)
 Definition pproduct {A : Type} (F : A -> pType) : pType
   := [forall (a : A), pointed_type (F a), ispointed_type o F].
@@ -170,6 +165,38 @@ Proof.
     apply point_eq.
 Defined.
 
+(** The projections from a pointed product are pointed maps. *)
+Definition pfst {A B : pType} : A * B ->* A
+  := Build_pMap (A * B) A fst idpath.
+
+Definition psnd {A B : pType} : A * B ->* B
+  := Build_pMap (A * B) B snd idpath.
+
+Definition pprod_corec {X Y} (Z : pType) (f : Z ->* X) (g : Z ->* Y)
+  : Z ->* (X * Y)
+  := Build_pMap Z (X * Y) (fun z => (f z, g z))
+      (path_prod' (point_eq _) (point_eq _)).
+
+Definition pprod_corec_beta_fst {X Y} (Z : pType) (f : Z ->* X) (g : Z ->* Y)
+  : pfst o* pprod_corec Z f g ==* f.
+Proof.
+  snrapply Build_pHomotopy.
+  1: reflexivity.
+  apply moveL_pV.
+  refine (concat_1p _ @ _^ @ (concat_p1 _)^).
+  apply ap_fst_path_prod'.
+Defined.
+
+Definition pprod_corec_beta_snd {X Y} (Z : pType) (f : Z ->* X) (g : Z ->* Y)
+  : psnd o* pprod_corec Z f g ==* g.
+Proof.
+  snrapply Build_pHomotopy.
+  1: reflexivity.
+  apply moveL_pV.
+  refine (concat_1p _ @ _^ @ (concat_p1 _)^).
+  apply ap_snd_path_prod'.
+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. *)
@@ -670,18 +697,9 @@ Proof.
   - exact (X * Y).
   - exact pfst.
   - exact psnd.
-  - intros Z f g.
-    snrapply Build_pMap.
-    1: exact (fun w => (f w, g w)).
-    apply path_prod'; cbn; apply point_eq.
-  - intros Z f g.
-    snrapply Build_pHomotopy.
-    1: reflexivity.
-    by pelim f g.
-  - intros Z f g.
-    snrapply Build_pHomotopy.
-    1: reflexivity.
-    by pelim f g.
+  - exact pprod_corec.
+  - exact pprod_corec_beta_fst.
+  - exact pprod_corec_beta_snd.
   - intros Z f g p q.
     simpl.
     snrapply Build_pHomotopy.

theories/Types/Prod.v

@@ -69,6 +69,13 @@ Proof.
   reflexivity.
 Defined.
 
+Definition ap_fst_path_prod' {A B : Type} {x x' : A} {y y' : B}
+  (p : x = x') (q : y = y')
+  : ap fst (path_prod' p q) = p.
+Proof.
+  apply ap_fst_path_prod.
+Defined.
+
 Definition ap_snd_path_prod {A B : Type} {z z' : A * B}
   (p : fst z = fst z') (q : snd z = snd z') :
   ap snd (path_prod _ _ p q) = q.
@@ -79,6 +86,13 @@ Proof.
   reflexivity.
 Defined.
 
+Definition ap_snd_path_prod' {A B : Type} {x x' : A} {y y' : B}
+  (p : x = x') (q : y = y')
+  : ap snd (path_prod' p q) = q.
+Proof.
+  apply ap_snd_path_prod.
+Defined.
+
 Definition eta_path_prod {A B : Type} {z z' : A * B} (p : z = z') :
   path_prod _ _(ap fst p) (ap snd p) = p.
 Proof.