Library HoTT.Homotopy.Wedge

Require Import Basics Types.
Require Import Pointed.Core Pointed.pSusp.
Require Import Colimits.Pushout.
Require Import WildCat.Coproducts WildCat.Products.
Require Import Homotopy.Suspension.
Require Import Truncations.Core Truncations.Connectedness.
Require Import Extensions Modalities.ReflectiveSubuniverse.

Wedge sums


Local Open Scope pointed_scope.

Definition Wedge@{i j k | i ≤ k, j ≤ k} (X : pType@{i}) (Y : pType@{j}) : pType@{k}
  := [Pushout@{Set i j k} (fun _ : Unit ⇒ point X) (fun _ ⇒ point Y), pushl (point X)].

Notation "X \/ Y" := (Wedge X Y) : pointed_scope.

Definition wglue {X Y : pType}
  : pushl (point X) = (pushr (point Y)) :> (X ∨ Y) := pglue tt.

Definition wedge_inl {X Y : pType} : X ->* X ∨ Y
  := Build_pMap _ _ pushl 1.

Definition wedge_inr {X Y : pType} : Y ->* X ∨ Y
  := Build_pMap _ _ pushr wglue^.

Wedge recursion into an unpointed type.
Definition wedge_rec' {X Y : pType} {Z : Type}
  (f : X → Z) (g : Y → Z) (w : f pt = g pt)
  : Wedge X Y → Z
  := Pushout_rec Z f g (fun _ ⇒ w).

Definition wedge_rec {X Y : pType} {Z : pType} (f : X ->* Z) (g : Y ->* Z)
  : X ∨ Y ->* Z
  := Build_pMap _ _ (wedge_rec' f g (point_eq f @ (point_eq g)^)) (point_eq f).

Definition wedge_rec_beta_wglue {X Y Z : pType} (f : X ->* Z) (g : Y ->* Z)
  : ap (wedge_rec f g) wglue = point_eq f @ (point_eq g)^
  := Pushout_rec_beta_pglue _ f g _ tt.

Definition wedge_rec_beta_inl {X Y : pType} {Z : pType} (f : X ->* Z) (g : Y ->* Z)
  : wedge_rec f g o× wedge_inl ==* f.
Proof.
  snapply Build_pHomotopy.
  1: reflexivity.
  cbn beta; symmetry.
  exact (concat_pp_V 1 (point_eq f)).
Defined.

Definition wedge_rec_beta_inr {X Y : pType} {Z : pType} (f : X ->* Z) (g : Y ->* Z)
  : wedge_rec f g o× wedge_inr ==* g.
Proof.
  snapply Build_pHomotopy.
  1: reflexivity.
  cbn -[wedge_rec].
  rhs napply concat_pp_p.
  rhs napply (ap_V _ _ @@ 1).
  apply moveL_Vp.
  lhs napply concat_p1.
  napply wedge_rec_beta_wglue.
Defined.

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.

Definition wedge_incl_beta_wglue {X Y : pType}
  : ap (@wedge_incl X Y) wglue = 1.
Proof.
  lhs_V napply eta_path_prod.
  napply (ap011 _ (x':=1) (y':=1)).
  - lhs_V napply (ap_compose (wedge_incl X Y) _ wglue).
    napply wedge_rec_beta_wglue.
  - lhs_V napply (ap_compose (wedge_incl X Y) _ wglue).
    napply wedge_rec_beta_wglue.
Defined.

Definition wedge_ind {X Y : pType} (P : X ∨ Y → Type)
  (f : ∀ x, P (wedge_inl x)) (g : ∀ y, P (wedge_inr y))
  (w : wglue # f pt = g pt)
  : ∀ xy, P xy.
Proof.
  napply (Pushout_ind P f g).
  intros [].
  exact w.
Defined.

Definition wedge_ind_beta_wglue {X Y : pType} (P : X ∨ Y → Type)
  (f : ∀ x, P (wedge_inl x)) (g : ∀ 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.
  napply (wedge_ind _ l r).
  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 : ∀ x, g (f (wedge_inl x)) = y)
  (r : ∀ x, g (f (wedge_inr x)) = y)
  (w : l pt = ap g (ap f wglue) @ r pt)
  : ∀ x, g (f x) = y.
Proof.
  napply (wedge_ind _ l r); simpl.
  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.
  napply (wedge_ind _ l r); simpl.
  transport_paths FFlr.
  exact w.
Defined.

1-universal property of wedge.
Lemma wedge_up X Y Z (f g : X ∨ Y ->* Z)
  (p : f o× wedge_inl ==* g o× wedge_inl)
  (q : f o× wedge_inr ==* g o× wedge_inr)
  : f ==* g.
Proof.
  snapply Build_pHomotopy.
  - napply (wedge_ind_FlFr p q).
    lhs napply (1 @@ dpoint_eq q).
    rhs napply (dpoint_eq p @@ 1).
    clear p q; simpl.
    rhs napply (((concat_1p _) @@ ap inverse (concat_1p _)) @@ 1).
    lhs napply concat_p_pp.
    apply moveR_pV.
    lhs napply (1 @@ (ap_V _ _ @@ 1)).
    lhs napply concat_p_Vp.
    rhs napply concat_p_pp.
    rhs napply ((1 @@ ap_V _ _) @@ 1).
    rhs napply (concat_pp_V _ _ @@ 1).
    by apply moveL_pM.
  - simpl.
    lhs exact (dpoint_eq p); simpl.
    exact (concat_1p _ @@ ap inverse (concat_1p _)).
Defined.

Instance hasbinarycoproducts : HasBinaryCoproducts pType.
Proof.
  intros X Y.
  snapply Build_BinaryCoproduct.
  - exact (X ∨ Y).
  - exact wedge_inl.
  - exact wedge_inr.
  - exact (@wedge_rec X Y).
  - exact (@wedge_rec_beta_inl X Y).
  - exact (@wedge_rec_beta_inr X Y).
  - exact (wedge_up X Y).
Defined.

Lemmas about wedge functions


Lemma wedge_pr1_inl {X Y} : wedge_pr1 o× (@wedge_inl X Y) ==* pmap_idmap.
Proof.
  reflexivity.
Defined.

Lemma wedge_pr1_inr {X Y} : wedge_pr1 o× (@wedge_inr X Y) ==* pconst.
Proof.
  snapply Build_pHomotopy.
  1: reflexivity.
  symmetry; simpl.
  do 2 lhs napply concat_p1.
  lhs napply (ap_V _ wglue).
  exact (inverse2 (wedge_rec_beta_wglue pmap_idmap pconst)).
Defined.

Lemma wedge_pr2_inl {X Y} : wedge_pr2 o× (@wedge_inl X Y) ==* pconst.
Proof.
  reflexivity.
Defined.

Lemma wedge_pr2_inr {X Y} : wedge_pr2 o× (@wedge_inr X Y) ==* pmap_idmap.
Proof.
  snapply Build_pHomotopy.
  1: reflexivity.
  symmetry; simpl.
  do 2 lhs napply concat_p1.
  lhs napply (ap_V _ wglue).
  exact (inverse2 (wedge_rec_beta_wglue pconst pmap_idmap)).
Defined.

Wedge of an indexed family of pointed types
Note that the index type is not necessarily 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.
  snapply Build_pType.
  - srefine (Pushout (A := I) (B := sig X) (C := pUnit) _ _).
    + exact (fun i ⇒ (i; pt)).
    + exact (fun _ ⇒ pt).
  - apply pushr.
    exact pt.
Defined.

Definition fwedge_in' (I : Type) (X : I → pType)
  : ∀ i, X i ->* FamilyWedge I X
  := 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)
  : 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)
  (f : ∀ i, X i ->* Z)
  : FamilyWedge I X ->* Z.
Proof.
  snapply Build_pMap.
  - snapply Pushout_rec.
    + exact (sig_rec f).
    + exact pconst.
    + intros i.
      exact (point_eq (f i)).
  - exact idpath.
Defined.

Instance hasallcoproducts_ptype : HasAllCoproducts pType.
Proof.
  intros I X.
  snapply Build_Coproduct.
  - exact (FamilyWedge I X).
  - exact (fwedge_in' I X).
  - exact (fwedge_rec I X).
  - intros Z f i.
    snapply 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.
    snapply Build_pHomotopy.
    + snapply Pushout_ind.
      × intros [i x].
        napply h.
      × intros [].
        exact (point_eq _ @ (point_eq _)^).
      × intros i; cbn.
        transport_paths FlFr.
        lhs napply concat_p_pp.
        apply moveR_pV.
        rhs napply concat_pp_p.
        apply moveL_pM.
        symmetry.
        exact (dpoint_eq (h i)).
    + reflexivity.
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 summand should land in.
Definition fwedge_incl `{Funext} (I : Type) `(DecidablePaths I) (X : I → pType)
  : FamilyWedge I X ->* pproduct X
  := cat_coprod_prod X.

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.
This is the image to keep in mind: 
                                    *
                                   /|\
                                  / | \
    Susp X                       /  |  \
                                /   |   \
       *                       * merid(x)*
      /|\                       \   |   /
     / | \                       \  |  /
    /  |  \                       \ | /
   /   |   \      Pinch            \|/
  * merid(x)*   ---------->         *
   \   |   /                       /|\
    \  |  /                       / | \
     \ | /                       /  |  \
      \|/                       /   |   \
       *                       * merid(x)*
                                \   |   /
                                 \  |  /
                                  \ | /
                                   \|/
                                    *
Note that this is only a conceptual picture as we aren't working with "reduced suspensions". This means we have to track back along merid pt making this map a little trickier to imagine.
The pinch map for a suspension.
Definition psusp_pinch (X : pType) : psusp X ->* psusp X ∨ psusp X.
Proof.
  refine (Build_pMap _ _ (Susp_rec pt pt _) idpath).
  intros x.
  refine (ap wedge_inl _ @ wglue @ ap wedge_inr _ @ wglue^).
  1,2: exact (loop_susp_unit X x).
Defined.

It should compute when aped on a merid.
Definition psusp_pinch_beta_merid {X : pType} (x : X)
  : ap (psusp_pinch X) (merid x)
    = ap wedge_inl (loop_susp_unit X x) @ wglue
    @ ap wedge_inr (loop_susp_unit X x) @ wglue^.
Proof.
  rapply Susp_rec_beta_merid.
Defined.

Doing wedge projections on the pinch map gives the identity.
Definition wedge_pr1_psusp_pinch {X}
  : wedge_pr1 o× psusp_pinch X ==* @pmap_idmap (psusp X).
Proof.
  snapply Build_pHomotopy.
  - snapply Susp_ind_FlFr.
    + reflexivity.
    + exact (merid pt).
    + intros x.
      rhs napply concat_1p.
      rhs napply ap_idmap.
      apply moveR_pM.
      change (?t = _) with (t = loop_susp_unit X x).
      lhs napply (ap_compose (psusp_pinch X)).
      lhs napply (ap _ (psusp_pinch_beta_merid x)).
      lhs napply ap_pV.
      apply moveR_pV.
      rhs napply (whiskerL _ (wedge_rec_beta_wglue _ _)).
      lhs napply ap_pp.
      lhs napply (ap (fun x ⇒ _ @ x)).
      { lhs_V napply ap_compose.
        apply ap_const. }
      lhs napply concat_p1.
      lhs napply ap_pp.
      lhs napply (ap (fun x ⇒ _ @ x) (wedge_rec_beta_wglue _ _)).
      f_ap.
      lhs_V napply (ap_compose wedge_inl).
      apply ap_idmap.
  - reflexivity.
Defined.

Definition wedge_pr2_psusp_pinch {X}
  : wedge_pr2 o× psusp_pinch X ==* @pmap_idmap (psusp X).
Proof.
  snapply Build_pHomotopy.
  - snapply Susp_ind_FlFr.
    + reflexivity.
    + exact (merid pt).
    + intros x.
      rhs napply concat_1p.
      rhs napply ap_idmap.
      apply moveR_pM.
      change (?t = _) with (t = loop_susp_unit X x).
      lhs napply (ap_compose (psusp_pinch X)).
      lhs napply (ap _ (psusp_pinch_beta_merid x)).
      lhs napply ap_pV.
      apply moveR_pV.
      rhs napply (whiskerL _ (wedge_rec_beta_wglue _ _)).
      lhs napply ap_pp.
      lhs napply (ap (fun x ⇒ _ @ x) _).
      { lhs_V napply ap_compose.
        apply ap_idmap. }
      rhs napply concat_p1.
      apply moveR_pM.
      lhs napply ap_pp.
      rhs napply concat_pV.
      lhs napply (ap _ (wedge_rec_beta_wglue _ _)).
      apply moveR_pM.
      lhs_V napply (ap_compose wedge_inl).
      rapply ap_const.
  - reflexivity.
Defined.

Connectivity of wedge inclusion


Definition extension_wedge_incl {X Y : pType} (P : X × Y → Type)
  (d : ∀ a : X ∨ Y, P (wedge_incl X Y a))
  (f : ∀ (x : X) (y : Y), P (x, y))
  (p : ∀ (x : X), f x pt = d (wedge_inl x))
  (q : ∀ (y : Y), f pt y = d (wedge_inr y))
  (pq : p pt
        = q pt
            @ ((apD d wglue)^
                 @ transport_compose_path_ap P (wedge_incl X Y) (wedge_incl_beta_wglue) _))
  : ExtensionAlong (wedge_incl X Y) P d.
Proof.
  ∃ (prod_ind _ f).
  napply (wedge_ind _ p q).
  lhs napply (transport_paths_FlFr_D wglue).
  apply moveR_pM.
  apply moveR_Vp.
  unshelve lhs napply ap_homotopic_id.
  1: exact (transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue).
  change (prod_ind P f (wedge_incl X Y (pushl pt))) with (f pt pt).
  apply moveR_pV.
  rhs napply concat_pp_p.
  rhs napply (1 @@ concat_pp_p _ _ _).
  nrefine (_ @@ pq).
  symmetry.
  lhs napply apD_compose.
  unfold transport_compose_path_ap.
  apply whiskerL.
  lhs napply (apD02 _ wedge_incl_beta_wglue).
  apply concat_p1.
Defined.

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.
  apply conn_map_from_extension_elim.
  intros P h d.
  snapply extension_wedge_incl.
  - rapply (wedge_incl_elim _ _ (fun x y ⇒ P (x, y)) (d o wedge_inr) (d o wedge_inl)).
    lhs_V exact (apD d wglue).
    exact (transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue _).
  - napply wedge_incl_comp2.
  - napply wedge_incl_comp1.
  - napply wedge_incl_comp3.
Defined.