connectivity of wedge inclusion

theories/Homotopy/Wedge.v

@@ -3,6 +3,8 @@ Require Import Pointed.Core Pointed.pSusp.
 Require Import Colimits.Pushout.
 Require Import WildCat.
 Require Import Homotopy.Suspension.
+Require Import Truncations.Core Truncations.Connectedness.
+Require Import Modalities.ReflectiveSubuniverse.
 
 Local Set Universe Minimization ToSet.
 
@@ -79,6 +81,56 @@ Proof.
   - reflexivity.
 Defined.
 
+Definition wedge_ind {X Y : pType} (P : X \/ Y -> Type)
+  (f : forall x, P (wedge_inl x)) (g : forall y, P (wedge_inr y))
+  (w : wglue # f pt = g pt)
+  : forall xy, P xy.
+Proof.
+  snrapply (Pushout_ind P f g).
+  intros [].
+  exact w.
+Defined.
+
+Definition wedge_ind_beta_wglue {X Y : pType} (P : X \/ Y -> Type)
+  (f : forall x, P (wedge_inl x)) (g : forall y, P (wedge_inr y))
+  (w : wglue # f pt = g pt)
+  : apD (wedge_ind P f g w) wglue = w
+  := Pushout_ind_beta_pglue P _ _ _ _.
+
+Definition wedge_ind_FlFr {X Y Z : pType} {f g : X \/ Y -> Z}
+  (l : f o wedge_inl == g o wedge_inl)
+  (r : f o wedge_inr == g o wedge_inr)
+  (w : ap f wglue @ r pt = l pt @ ap g wglue)
+  : f == g.
+Proof.
+  snrapply (wedge_ind _ l r).
+  nrapply transport_paths_FlFr'.
+  exact w.
+Defined.
+
+Definition wedge_ind_FFl {X Y Z W : pType} (f : X \/ Y -> Z) (g : Z -> W)
+  {y : W}
+  (l : forall x, g (f (wedge_inl x)) = y)
+  (r : forall x, g (f (wedge_inr x)) = y)
+  (w : ap g (ap f wglue) @ r pt = l pt)
+  : forall x, g (f x) = y.
+Proof.
+  snrapply (wedge_ind _ l r); simpl.
+  nrapply transport_paths_FFl'.
+  exact w.
+Defined.
+
+Definition wedge_ind_FFlr {X Y Z : pType} (f : X \/ Y -> Z) (g : Z -> X \/ Y)
+  (l : g o f o wedge_inl == wedge_inl)
+  (r : g o f o wedge_inr == wedge_inr)
+  (w : ap g (ap f wglue) @ r pt = l pt @ wglue)
+  : g o f == idmap. 
+Proof.
+  snrapply (wedge_ind _ l r); simpl.
+  nrapply transport_paths_FFlr'.
+  exact w.
+Defined.
+
 (** 1-universal property of wedge. *)
 Lemma wedge_up X Y Z (f g : X \/ Y $-> Z)
   : f $o wedge_inl $== g $o wedge_inl
@@ -87,9 +139,7 @@ Lemma wedge_up X Y Z (f g : X \/ Y $-> Z)
 Proof.
   intros p q.
   snrapply Build_pHomotopy.
-  - snrapply (Pushout_ind _ p q).
-    intros [].
-    nrapply transport_paths_FlFr'.
+  - snrapply (wedge_ind_FlFr p q).
     lhs nrapply (whiskerL _ (dpoint_eq q)).
     rhs nrapply (whiskerR (dpoint_eq p)).
     clear p q.
@@ -131,7 +181,7 @@ Proof.
   - intros Z f g.
     snrapply Build_pHomotopy.
     1: reflexivity.
-    by simpl; pelim f.
+    symmetry; apply concat_pp_V.
   - intros Z f g.
     snrapply Build_pHomotopy.
     1: reflexivity.
@@ -142,9 +192,9 @@ Proof.
     apply moveR_Mp.
     apply moveL_pV.
     apply moveR_Vp.
-    refine (Pushout_rec_beta_pglue _ f g _ _  @ _).
-    simpl.
-    by pelim f g.
+    lhs nrapply wedge_rec_beta_wglue.
+    f_ap; f_ap; symmetry.
+    apply concat_1p.
   - intros Z f g p q.
     by apply wedge_up.
 Defined.
@@ -370,3 +420,64 @@ Proof.
   - reflexivity.
 Defined.
 
+(** ** Connectivity of wedge inclusion *)
+
+Definition conn_map_wedge_incl `{Univalence} {m n : trunc_index} (X Y : pType)
+  `{!IsConnected m.+1 X, !IsConnected n.+1 Y}
+  : IsConnMap (m +2+ n) (wedge_incl X Y).
+Proof.
+  rewrite trunc_index_add_comm.
+  apply conn_map_from_extension_elim.
+  intros P h d.
+  transparent assert (f : (forall x y, P (x, y))). 
+  { intros x y; revert y x.
+    rapply (wedge_incl_elim (n:=m) (m:=n)
+      (point Y) (point X) (fun y x => P (x, y))
+      (d o wedge_inl) (d o wedge_inr)).
+    rhs_V nrapply (apD d wglue).
+    rhs nrapply transport_compose.
+    nrapply (transport2 _ (p:=1) _^).
+    apply wedge_incl_beta_wglue. }
+  transparent assert (p : (forall x : X,
+    prod_ind P f (wedge_incl X Y (wedge_inl x)) = d (wedge_inl x))).
+  1: nrapply wedge_incl_comp1.
+  transparent assert (q : (forall y : Y,
+    prod_ind P f (wedge_incl X Y (wedge_inr y)) = d (wedge_inr y))).
+  1: nrapply wedge_incl_comp2.
+  transparent assert (pq
+    : (q pt = p pt @
+      ((transport2 P wedge_incl_beta_wglue^ (d (wedge_inl pt))
+        @ (transport_compose P (wedge_incl X Y) wglue (d (pushl pt)))^)
+      @ apD d wglue))).
+  1: nrapply wedge_incl_comp3.
+  clearbody f p q pq.
+  exists (prod_ind _ f).
+  nrapply (wedge_ind _ p q).
+  rhs nrapply pq.
+  lhs nrapply (transport_paths_FlFr_D wglue).
+  lhs nrapply concat_pp_p.
+  apply moveR_Vp.
+  rhs nrapply concat_p_pp.
+  rhs nrapply concat_p_pp.
+  apply whiskerR.
+  unshelve lhs nrapply ap_homotopic_id.
+  { intros x.
+    lhs nrapply transport_compose.
+    nrapply (transport2 _ (q:=1)).
+    apply wedge_incl_beta_wglue. }
+  cbn beta.
+  apply concat2.
+  - apply whiskerR.
+    symmetry.
+    lhs nrapply apD_compose.
+    apply whiskerL.
+    lhs_V nrapply (apD _ wedge_incl_beta_wglue^).
+    nrapply moveR_transport_V.
+    symmetry.
+    nrapply (transport_paths_Fl' wedge_incl_beta_wglue).
+    nrapply concat_p1.
+  - symmetry.
+    rhs nrapply inv_pp.
+    apply whiskerR.
+    exact (transport2_V P wedge_incl_beta_wglue _).
+Defined.

theories/Types/Paths.v

@@ -140,6 +140,25 @@ Proof.
   exact h^.
 Defined.
 
+Definition transport_paths_Fl' {A B : Type} {f : A -> B} {x1 x2 : A} {y : B}
+  (p : x1 = x2) (q : f x1 = y) (r : f x2 = y) (h : ap f p @ r = q)
+  : transport (fun x => f x = y) p q = r.
+Proof.
+  refine (transport_paths_Fl _ _ @ _).
+  apply moveR_Vp.
+  exact h^.
+Defined.
+
+Definition transport_paths_FFl' {A B C : Type} {f : A -> B} {g : B -> C}
+  {x1 x2 : A} {y : C} (p : x1 = x2) (q : g (f x1) = y) (r : g (f x2) = y)
+  (h : ap g (ap f p) @ r = q)
+  : transport (fun x => g (f x) = y) p q = r.
+Proof.
+  refine (transport_paths_FFl _ _ @ _).
+  apply moveR_Vp.
+  exact h^.
+Defined.
+
 Definition transport_paths_FlFr' {A B : Type} {f g : A -> B} {x1 x2 : A}
   (p : x1 = x2) (q : f x1 = g x1) (r : (f x2) = (g x2))
   (h : (ap f p) @ r = q @ (ap g p))