From HoTT Require Import Basics Types.From HoTT 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.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
wedge_rec f g o* wedge_inl ==* f
Proof.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
wedge_rec f g o* wedge_inl ==* f
  snapply Build_pHomotopy.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
wedge_rec f g o* wedge_inl == f
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
?p pt = dpoint_eq (wedge_rec f g o* wedge_inl) @ (dpoint_eq f)^
  1: reflexivity.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
(fun x0 : X => 1) pt =
dpoint_eq (wedge_rec f g o* wedge_inl) @ (dpoint_eq f)^
  cbn beta; symmetry.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
dpoint_eq (wedge_rec f g o* wedge_inl) @ (dpoint_eq f)^ = 1
  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.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
wedge_rec f g o* wedge_inr ==* g
Proof.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
wedge_rec f g o* wedge_inr ==* g
  snapply Build_pHomotopy.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
wedge_rec f g o* wedge_inr == g
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
?p pt = dpoint_eq (wedge_rec f g o* wedge_inr) @ (dpoint_eq g)^
  1: reflexivity.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
(fun x0 : Y => 1) pt =
dpoint_eq (wedge_rec f g o* wedge_inr) @ (dpoint_eq g)^
  cbn -[wedge_rec].
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
1 = (ap (wedge_rec f g) wglue^ @ point_eq (wedge_rec f g)) @ (dpoint_eq g)^
  rhs napply concat_pp_p.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
1 = ap (wedge_rec f g) wglue^ @ (point_eq (wedge_rec f g) @ (dpoint_eq g)^)
  rhs napply (ap_V _ _ @@ 1).
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
1 = (ap (wedge_rec f g) wglue)^ @ (point_eq (wedge_rec f g) @ (dpoint_eq g)^)
  apply moveL_Vp.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
ap (wedge_rec f g) wglue @ 1 = point_eq (wedge_rec f g) @ (dpoint_eq g)^
  lhs napply concat_p1.
X, Y, Z: pType
f: X ->* Z
g: Y ->* Z
ap (wedge_rec f g) wglue = point_eq (wedge_rec f g) @ (dpoint_eq g)^
  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.
X, Y: pType
ap (wedge_incl X Y) wglue = 1
Proof.
X, Y: pType
ap (wedge_incl X Y) wglue = 1
  lhs_V napply eta_path_prod.
X, Y: pType
path_prod (wedge_incl X Y (pushl pt)) (wedge_incl X Y (pushr pt))
  (ap fst (ap (wedge_incl X Y) wglue)) (ap snd (ap (wedge_incl X Y) wglue)) =
1
  napply (ap011 _ (x':=1) (y':=1)).
X, Y: pType
ap fst (ap (wedge_incl X Y) wglue) = 1
X, Y: pType
ap snd (ap (wedge_incl X Y) wglue) = 1
  -
X, Y: pType
ap fst (ap (wedge_incl X Y) wglue) = 1 lhs_V napply (ap_compose (wedge_incl X Y) _ wglue).
X, Y: pType
ap (fun x : X \/ Y => fst (wedge_incl X Y x)) wglue = 1
    napply wedge_rec_beta_wglue.
  -
X, Y: pType
ap snd (ap (wedge_incl X Y) wglue) = 1 lhs_V napply (ap_compose (wedge_incl X Y) _ wglue).
X, Y: pType
ap (fun x : X \/ Y => snd (wedge_incl X Y x)) wglue = 1
    napply wedge_rec_beta_wglue.
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.
X, Y: pType
P: X \/ Y -> Type
f: forall x : X, P (wedge_inl x)
g: forall y : Y, P (wedge_inr y)
w: transport P wglue (f pt) = g pt
forall xy : X \/ Y, P xy
Proof.
X, Y: pType
P: X \/ Y -> Type
f: forall x : X, P (wedge_inl x)
g: forall y : Y, P (wedge_inr y)
w: transport P wglue (f pt) = g pt
forall xy : X \/ Y, P xy
  napply (Pushout_ind P f g).
X, Y: pType
P: X \/ Y -> Type
f: forall x : X, P (wedge_inl x)
g: forall y : Y, P (wedge_inr y)
w: transport P wglue (f pt) = g pt
forall a : Unit, transport P (pglue a) (f pt) = g pt
  intros [].
X, Y: pType
P: X \/ Y -> Type
f: forall x : X, P (wedge_inl x)
g: forall y : Y, P (wedge_inr y)
w: transport P wglue (f pt) = g pt
transport P (pglue tt) (f pt) = g pt
  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.
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.
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
  napply (wedge_ind _ l r).
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
transport (fun xy : X \/ Y => f xy = g xy) wglue (l pt) = r pt
  transport_paths 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
ap f wglue @ r pt = l pt @ ap g wglue
  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 : l pt = ap g (ap f wglue) @ r pt)
  : forall x, g (f x) = y.
X, Y, Z, W: pType
f: X \/ Y -> Z
g: Z -> W
y: W
l: forall x : X, g (f (wedge_inl x)) = y
r: forall x : Y, g (f (wedge_inr x)) = y
w: l pt = ap g (ap f wglue) @ r pt
forall x : X \/ Y, g (f x) = y
Proof.
X, Y, Z, W: pType
f: X \/ Y -> Z
g: Z -> W
y: W
l: forall x : X, g (f (wedge_inl x)) = y
r: forall x : Y, g (f (wedge_inr x)) = y
w: l pt = ap g (ap f wglue) @ r pt
forall x : X \/ Y, g (f x) = y
  napply (wedge_ind _ l r); simpl.
X, Y, Z, W: pType
f: X \/ Y -> Z
g: Z -> W
y: W
l: forall x : X, g (f (wedge_inl x)) = y
r: forall x : Y, g (f (wedge_inr x)) = y
w: l pt = ap g (ap f wglue) @ r pt
transport (fun xy : Pushout (unit_name pt) (unit_name pt) => g (f xy) = y)
  wglue (l pt) =
r pt
  transport_paths FFl.
X, Y, Z, W: pType
f: X \/ Y -> Z
g: Z -> W
y: W
l: forall x : X, g (f (wedge_inl x)) = y
r: forall x : Y, g (f (wedge_inr x)) = y
w: l pt = ap g (ap f wglue) @ r pt
l pt = ap g (ap f wglue) @ r pt
  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.
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.
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
  napply (wedge_ind _ l r); simpl.
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
transport (fun xy : Pushout (unit_name pt) (unit_name pt) => g (f xy) = xy)
  wglue (l pt) =
r pt
  transport_paths 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
ap g (ap f wglue) @ r pt = l pt @ wglue
  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.
X, Y, Z: pType
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.
X, Y, Z: pType
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
  snapply Build_pHomotopy.
X, Y, Z: pType
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
X, Y, Z: pType
f, g: X \/ Y ->* Z
p: f o* wedge_inl ==* g o* wedge_inl
q: f o* wedge_inr ==* g o* wedge_inr
?p pt = dpoint_eq f @ (dpoint_eq g)^
  -
X, Y, Z: pType
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 napply (wedge_ind_FlFr p q).
X, Y, Z: pType
f, g: X \/ Y ->* Z
p: f o* wedge_inl ==* g o* wedge_inl
q: f o* wedge_inr ==* g o* wedge_inr
ap f wglue @ q pt = p pt @ ap g wglue
    lhs napply (1 @@ dpoint_eq q).
X, Y, Z: pType
f, g: X \/ Y ->* Z
p: f o* wedge_inl ==* g o* wedge_inl
q: f o* wedge_inr ==* g o* wedge_inr
ap f wglue @ dpoint (pfam_phomotopy (f o* wedge_inr) (g o* wedge_inr)) =
p pt @ ap g wglue
    rhs napply (dpoint_eq p @@ 1).
X, Y, Z: pType
f, g: X \/ Y ->* Z
p: f o* wedge_inl ==* g o* wedge_inl
q: f o* wedge_inr ==* g o* wedge_inr
ap f wglue @ dpoint (pfam_phomotopy (f o* wedge_inr) (g o* wedge_inr)) =
dpoint (pfam_phomotopy (f o* wedge_inl) (g o* wedge_inl)) @ ap g wglue
    clear p q; simpl.
X, Y, Z: pType
f, g: X \/ Y ->* Z
ap f wglue @ ((ap f wglue^ @ point_eq f) @ (ap g wglue^ @ point_eq g)^) =
((1 @ point_eq f) @ (1 @ point_eq g)^) @ ap g wglue
    rhs napply (((concat_1p _) @@ ap inverse (concat_1p _)) @@ 1).
X, Y, Z: pType
f, g: X \/ Y ->* Z
ap f wglue @ ((ap f wglue^ @ point_eq f) @ (ap g wglue^ @ point_eq g)^) =
(point_eq f @ (point_eq g)^) @ ap g wglue
    lhs napply concat_p_pp.
X, Y, Z: pType
f, g: X \/ Y ->* Z
(ap f wglue @ (ap f wglue^ @ point_eq f)) @ (ap g wglue^ @ point_eq g)^ =
(point_eq f @ (point_eq g)^) @ ap g wglue
    apply moveR_pV.
X, Y, Z: pType
f, g: X \/ Y ->* Z
ap f wglue @ (ap f wglue^ @ point_eq f) =
((point_eq f @ (point_eq g)^) @ ap g wglue) @ (ap g wglue^ @ point_eq g)
    lhs napply (1 @@ (ap_V _ _ @@ 1)).
X, Y, Z: pType
f, g: X \/ Y ->* Z
ap f wglue @ ((ap f wglue)^ @ point_eq f) =
((point_eq f @ (point_eq g)^) @ ap g wglue) @ (ap g wglue^ @ point_eq g)
    lhs napply concat_p_Vp.
X, Y, Z: pType
f, g: X \/ Y ->* Z
point_eq f =
((point_eq f @ (point_eq g)^) @ ap g wglue) @ (ap g wglue^ @ point_eq g)
    rhs napply concat_p_pp.
X, Y, Z: pType
f, g: X \/ Y ->* Z
point_eq f =
(((point_eq f @ (point_eq g)^) @ ap g wglue) @ ap g wglue^) @ point_eq g
    rhs napply ((1 @@ ap_V _ _) @@ 1).
X, Y, Z: pType
f, g: X \/ Y ->* Z
point_eq f =
(((point_eq f @ (point_eq g)^) @ ap g wglue) @ (ap g wglue)^) @ point_eq g
    rhs napply (concat_pp_V _ _ @@ 1).
X, Y, Z: pType
f, g: X \/ Y ->* Z
point_eq f = (point_eq f @ (point_eq g)^) @ point_eq g
    by apply moveL_pM.
  -
X, Y, Z: pType
f, g: X \/ Y ->* Z
p: f o* wedge_inl ==* g o* wedge_inl
q: f o* wedge_inr ==* g o* wedge_inr
wedge_ind_FlFr p q
  ((1 @@ dpoint_eq q) @
   (((concat_p_pp (ap f wglue) (ap f wglue^ @ point_eq f)
        (ap g wglue^ @ point_eq g)^ @
      moveR_pV (ap g wglue^ @ point_eq g)
        ((point_eq f @ (point_eq g)^) @ ap g wglue)
        (ap f wglue @ (ap f wglue^ @ point_eq f))
        ((1 @@ (ap_V f wglue @@ 1)) @
         (concat_p_Vp (ap f wglue) (point_eq f) @
          (((moveL_pM (point_eq g) (point_eq f) (point_eq f @ (point_eq g)^)
               1 @
             (concat_pp_V (point_eq f @ (point_eq g)^) (ap g wglue) @@ 1)^) @
            ((1 @@ ap_V g wglue) @@ 1)^) @
           (concat_p_pp ((point_eq f @ (point_eq g)^) @ ap g wglue)
              (ap g wglue^) (point_eq g))^)))) @
     ((concat_1p (point_eq f) @@ ap inverse (concat_1p (point_eq g))) @@ 1)^
     :
     ap f wglue @ dpoint (pfam_phomotopy (f o* wedge_inr) (g o* wedge_inr)) =
     dpoint (pfam_phomotopy (f o* wedge_inl) (g o* wedge_inl)) @ ap g wglue) @
    (dpoint_eq p @@ 1)^))
  pt =
dpoint_eq f @ (dpoint_eq g)^ simpl.
X, Y, Z: pType
f, g: X \/ Y ->* Z
p: f o* wedge_inl ==* g o* wedge_inl
q: f o* wedge_inr ==* g o* wedge_inr
p pt = dpoint_eq f @ (dpoint_eq g)^
    lhs exact (dpoint_eq p); simpl.
X, Y, Z: pType
f, g: X \/ Y ->* Z
p: f o* wedge_inl ==* g o* wedge_inl
q: f o* wedge_inr ==* g o* wedge_inr
(1 @ point_eq f) @ (1 @ point_eq g)^ = dpoint_eq f @ (dpoint_eq g)^
    exact (concat_1p _ @@ ap inverse (concat_1p _)).
Defined.

Instance hasbinarycoproducts : HasBinaryCoproducts pType.
HasBinaryCoproducts pType
Proof.
HasBinaryCoproducts pType
  intros X Y.
X, Y: pType
BinaryCoproduct X Y
  snapply Build_BinaryCoproduct.
X, Y: pType
pType
X, Y: pType
Core.Hom X ?cat_coprod
X, Y: pType
Core.Hom Y ?cat_coprod
X, Y: pType
forall z : pType, Core.Hom X z -> Core.Hom Y z -> Core.Hom ?cat_coprod z
X, Y: pType
forall (z : pType) (f : Core.Hom X z) (g : Core.Hom Y z),
Core.GpdHom (Core.cat_comp (?cat_coprod_rec z f g) ?cat_inl) f
X, Y: pType
forall (z : pType) (f : Core.Hom X z) (g : Core.Hom Y z),
Core.GpdHom (Core.cat_comp (?cat_coprod_rec z f g) ?cat_inr) g
X, Y: pType
forall (z : pType) (f g : Core.Hom ?cat_coprod z),
Core.GpdHom (Core.cat_comp f ?cat_inl) (Core.cat_comp g ?cat_inl) ->
Core.GpdHom (Core.cat_comp f ?cat_inr) (Core.cat_comp g ?cat_inr) ->
Core.GpdHom f g
  -
X, Y: pType
pType exact (X \/ Y).
  -
X, Y: pType
Core.Hom X (X \/ Y) exact wedge_inl.
  -
X, Y: pType
Core.Hom Y (X \/ Y) exact wedge_inr.
  -
X, Y: pType
forall z : pType, Core.Hom X z -> Core.Hom Y z -> Core.Hom (X \/ Y) z exact (@wedge_rec X Y).
  -
X, Y: pType
forall (z : pType) (f : Core.Hom X z) (g : Core.Hom Y z),
Core.GpdHom (Core.cat_comp (wedge_rec f g) wedge_inl) f exact (@wedge_rec_beta_inl X Y).
  -
X, Y: pType
forall (z : pType) (f : Core.Hom X z) (g : Core.Hom Y z),
Core.GpdHom (Core.cat_comp (wedge_rec f g) wedge_inr) g exact (@wedge_rec_beta_inr X Y).
  -
X, Y: pType
forall (z : pType) (f g : Core.Hom (X \/ Y) z),
Core.GpdHom (Core.cat_comp f wedge_inl) (Core.cat_comp g wedge_inl) ->
Core.GpdHom (Core.cat_comp f wedge_inr) (Core.cat_comp g wedge_inr) ->
Core.GpdHom f g 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.
X, Y: pType
wedge_pr1 o* wedge_inl ==* pmap_idmap
Proof.
X, Y: pType
wedge_pr1 o* wedge_inl ==* pmap_idmap
  reflexivity.
Defined.

Lemma wedge_pr1_inr {X Y} : wedge_pr1 o* (@wedge_inr X Y) ==* pconst.
X, Y: pType
wedge_pr1 o* wedge_inr ==* pconst
Proof.
X, Y: pType
wedge_pr1 o* wedge_inr ==* pconst
  snapply Build_pHomotopy.
X, Y: pType
wedge_pr1 o* wedge_inr == pconst
X, Y: pType
?p pt = dpoint_eq (wedge_pr1 o* wedge_inr) @ (dpoint_eq pconst)^
  1: reflexivity.
X, Y: pType
(fun x0 : Y => 1) pt =
dpoint_eq (wedge_pr1 o* wedge_inr) @ (dpoint_eq pconst)^
  symmetry; simpl.
X, Y: pType
(ap (wedge_rec' idmap (fun _ : Y => pt) 1) wglue^ @ 1) @ 1 = 1
  do 2 lhs napply concat_p1.
X, Y: pType
ap (wedge_rec' idmap (fun _ : Y => pt) 1) wglue^ = 1
  lhs napply (ap_V _ wglue).
X, Y: pType
(ap (wedge_rec' idmap (fun _ : Y => pt) 1) wglue)^ = 1
  exact (inverse2 (wedge_rec_beta_wglue pmap_idmap pconst)).
Defined.

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

Lemma wedge_pr2_inr {X Y} : wedge_pr2 o* (@wedge_inr X Y) ==* pmap_idmap.
X, Y: pType
wedge_pr2 o* wedge_inr ==* pmap_idmap
Proof.
X, Y: pType
wedge_pr2 o* wedge_inr ==* pmap_idmap
  snapply Build_pHomotopy.
X, Y: pType
wedge_pr2 o* wedge_inr == pmap_idmap
X, Y: pType
?p pt = dpoint_eq (wedge_pr2 o* wedge_inr) @ (dpoint_eq pmap_idmap)^
  1: reflexivity.
X, Y: pType
(fun x0 : Y => 1) pt =
dpoint_eq (wedge_pr2 o* wedge_inr) @ (dpoint_eq pmap_idmap)^
  symmetry; simpl.
X, Y: pType
(ap (wedge_rec' (fun _ : X => pt) idmap 1) wglue^ @ 1) @ 1 = 1
  do 2 lhs napply concat_p1.
X, Y: pType
ap (wedge_rec' (fun _ : X => pt) idmap 1) wglue^ = 1
  lhs napply (ap_V _ wglue).
X, Y: pType
(ap (wedge_rec' (fun _ : X => pt) idmap 1) wglue)^ = 1
  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.
I: Type
X: I -> pType
pType
Proof.
I: Type
X: I -> pType
pType
  snapply Build_pType.
I: Type
X: I -> pType
Type
I: Type
X: I -> pType
IsPointed ?pointed_type
  -
I: Type
X: I -> pType
Type srefine (Pushout (A := I) (B := sig X) (C := pUnit) _ _).
I: Type
X: I -> pType
I -> {x : I & X x}
I: Type
X: I -> pType
I -> pUnit
    +
I: Type
X: I -> pType
I -> {x : I & X x} exact (fun i => (i; pt)).
    +
I: Type
X: I -> pType
I -> pUnit exact (fun _ => pt).
  -
I: Type
X: I -> pType
IsPointed (Pushout (fun i : I => (i; pt)) (fun _ : I => pt)) apply pushr.
I: Type
X: I -> pType
pUnit
    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 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 : forall i, X i ->* Z)
  : FamilyWedge I X ->* Z.
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i ->* Z
FamilyWedge I X ->* Z
Proof.
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i ->* Z
FamilyWedge I X ->* Z
  snapply Build_pMap.
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i ->* Z
FamilyWedge I X -> Z
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i ->* Z
?f pt = pt
  -
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i ->* Z
FamilyWedge I X -> Z snapply Pushout_rec.
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i ->* Z
{x : I & X x} -> Z
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i ->* Z
pUnit -> Z
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i ->* Z
forall a : I,
?pushb ((fun i : I => (i; pt)) a) = ?pushc ((fun _ : I => pt) a)
    +
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i ->* Z
{x : I & X x} -> Z exact (sig_rec f).
    +
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i ->* Z
pUnit -> Z exact pconst.
    +
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i ->* Z
forall a : I,
sig_rec (fun i : I => f i) ((fun i : I => (i; pt)) a) =
pconst ((fun _ : I => pt) a) intros i.
I: Type
X: I -> pType
Z: pType
f: forall i0 : I, X i0 ->* Z
i: I
sig_rec (fun i0 : I => f i0) ((fun i0 : I => (i0; pt)) i) =
pconst ((fun _ : I => pt) i)
      exact (point_eq (f i)).
  -
I: Type
X: I -> pType
Z: pType
f: forall i : I, X i ->* Z
Pushout_rec Z (sig_rec (fun i : I => f i)) pconst
  (fun i : I => point_eq (f i)) pt =
pt exact idpath.
Defined.

Instance hasallcoproducts_ptype : HasAllCoproducts pType.
HasAllCoproducts pType
Proof.
HasAllCoproducts pType
  intros I X.
I: Type
X: I -> pType
Coproduct I X
  snapply Build_Coproduct.
I: Type
X: I -> pType
pType
I: Type
X: I -> pType
forall i : I, Core.Hom (X i) ?cat_coprod
I: Type
X: I -> pType
forall z : pType, (forall i : I, Core.Hom (X i) z) -> Core.Hom ?cat_coprod z
I: Type
X: I -> pType
forall (z : pType) (f : forall i : I, Core.Hom (X i) z) 
(i : I), Core.GpdHom (Core.cat_comp (?cat_coprod_rec z f) (?cat_in i)) (f i)
I: Type
X: I -> pType
forall (z : pType) (f g : Core.Hom ?cat_coprod z),
(forall i : I,
 Core.GpdHom (Core.cat_comp f (?cat_in i)) (Core.cat_comp g (?cat_in i))) ->
Core.GpdHom f g
  -
I: Type
X: I -> pType
pType exact (FamilyWedge I X).
  -
I: Type
X: I -> pType
forall i : I, Core.Hom (X i) (FamilyWedge I X) exact (fwedge_in' I X).
  -
I: Type
X: I -> pType
forall z : pType,
(forall i : I, Core.Hom (X i) z) -> Core.Hom (FamilyWedge I X) z exact (fwedge_rec I X).
  -
I: Type
X: I -> pType
forall (z : pType) (f : forall i : I, Core.Hom (X i) z) 
(i : I),
Core.GpdHom (Core.cat_comp (fwedge_rec I X z f) (fwedge_in' I X i)) (f i) intros Z f i.
I: Type
X: I -> pType
Z: pType
f: forall i0 : I, Core.Hom (X i0) Z
i: I
Core.GpdHom (Core.cat_comp (fwedge_rec I X Z f) (fwedge_in' I X i)) (f i)
    snapply Build_pHomotopy.
I: Type
X: I -> pType
Z: pType
f: forall i0 : I, Core.Hom (X i0) Z
i: I
Core.cat_comp (fwedge_rec I X Z f) (fwedge_in' I X i) == f i
I: Type
X: I -> pType
Z: pType
f: forall i0 : I, Core.Hom (X i0) Z
i: I
?p pt =
dpoint_eq (Core.cat_comp (fwedge_rec I X Z f) (fwedge_in' I X i)) @
(dpoint_eq (f i))^
    1: reflexivity.
I: Type
X: I -> pType
Z: pType
f: forall i0 : I, Core.Hom (X i0) Z
i: I
(fun x0 : X i => 1) pt =
dpoint_eq (Core.cat_comp (fwedge_rec I X Z f) (fwedge_in' I X i)) @
(dpoint_eq (f i))^
    simpl.
I: Type
X: I -> pType
Z: pType
f: forall i0 : I, Core.Hom (X i0) Z
i: I
1 =
(ap
   (Pushout_rec Z (sig_rec (fun i0 : I => f i0)) (unit_name pt)
      (fun i0 : I => point_eq (f i0)))
   (pglue i) @
 1) @
(dpoint_eq (f i))^
    apply moveL_pV.
I: Type
X: I -> pType
Z: pType
f: forall i0 : I, Core.Hom (X i0) Z
i: I
1 @ dpoint_eq (f i) =
ap
  (Pushout_rec Z (sig_rec (fun i0 : I => f i0)) (unit_name pt)
     (fun i0 : I => point_eq (f i0)))
  (pglue i) @
1
    apply equiv_1p_q1.
I: Type
X: I -> pType
Z: pType
f: forall i0 : I, Core.Hom (X i0) Z
i: I
dpoint_eq (f i) =
ap
  (Pushout_rec Z (sig_rec (fun i0 : I => f i0)) (unit_name pt)
     (fun i0 : I => point_eq (f i0)))
  (pglue i)
    symmetry.
I: Type
X: I -> pType
Z: pType
f: forall i0 : I, Core.Hom (X i0) Z
i: I
ap
  (Pushout_rec Z (sig_rec (fun i0 : I => f i0)) (unit_name pt)
     (fun i0 : I => point_eq (f i0)))
  (pglue i) =
dpoint_eq (f i)
    exact (Pushout_rec_beta_pglue Z _ (unit_name pt) (fun i => point_eq (f i)) _).
  -
I: Type
X: I -> pType
forall (z : pType) (f g : Core.Hom (FamilyWedge I X) z),
(forall i : I,
 Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
   (Core.cat_comp g (fwedge_in' I X i))) ->
Core.GpdHom f g intros Z f g h.
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (fwedge_in' I X i))
Core.GpdHom f g
    snapply Build_pHomotopy.
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (fwedge_in' I X i))
f == g
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (fwedge_in' I X i))
?p pt = dpoint_eq f @ (dpoint_eq g)^
    +
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (fwedge_in' I X i))
f == g snapply Pushout_ind.
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (fwedge_in' I X i))
forall b : {x : I & X x},
(fun w : Pushout (fun i : I => (i; pt)) (fun _ : I => pt) => f w = g w)
  (pushl b)
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (fwedge_in' I X i))
forall c : pUnit,
(fun w : Pushout (fun i : I => (i; pt)) (fun _ : I => pt) => f w = g w)
  (pushr c)
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (fwedge_in' I X i))
forall a : I,
transport
  (fun w : Pushout (fun i : I => (i; pt)) (fun _ : I => pt) => f w = g w)
  (pglue a) (?pushb ((fun i : I => (i; pt)) a)) =
?pushc ((fun _ : I => pt) a)
      *
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (fwedge_in' I X i))
forall b : {x : I & X x},
(fun w : Pushout (fun i : I => (i; pt)) (fun _ : I => pt) => f w = g w)
  (pushl b) intros [i x].
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i0 : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i0))
  (Core.cat_comp g (fwedge_in' I X i0))
i: I
x: X i
f (pushl (i; x)) = g (pushl (i; x))
        napply h.
      *
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (fwedge_in' I X i))
forall c : pUnit,
(fun w : Pushout (fun i : I => (i; pt)) (fun _ : I => pt) => f w = g w)
  (pushr c) intros [].
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (fwedge_in' I X i))
f (pushr tt) = g (pushr tt)
        exact (point_eq _ @ (point_eq _)^).
      *
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (fwedge_in' I X i))
forall a : I,
transport
  (fun w : Pushout (fun i : I => (i; pt)) (fun _ : I => pt) => f w = g w)
  (pglue a)
  ((fun b : {x : I & X x} => (fun (i : I) (x : X i) => h i x) b.1 b.2)
     ((fun i : I => (i; pt)) a)) =
(fun c : pUnit =>
 match c as u return (f (pushr u) = g (pushr u)) with
 | tt => point_eq f @ (point_eq g)^
 end) ((fun _ : I => pt) a) intros i; cbn.
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i0 : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i0))
  (Core.cat_comp g (fwedge_in' I X i0))
i: I
transport
  (fun w : Pushout (fun i0 : I => (i0; pt)) (fun _ : I => pt) => f w = g w)
  (pglue i) (h i pt) =
point_eq f @ (point_eq g)^
        transport_paths FlFr.
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i0 : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i0))
  (Core.cat_comp g (fwedge_in' I X i0))
i: I
ap f (pglue i) @ (point_eq f @ (point_eq g)^) = h i pt @ ap g (pglue i)
        lhs napply concat_p_pp.
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i0 : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i0))
  (Core.cat_comp g (fwedge_in' I X i0))
i: I
(ap f (pglue i) @ point_eq f) @ (point_eq g)^ = h i pt @ ap g (pglue i)
        apply moveR_pV.
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i0 : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i0))
  (Core.cat_comp g (fwedge_in' I X i0))
i: I
ap f (pglue i) @ point_eq f = (h i pt @ ap g (pglue i)) @ point_eq g
        rhs napply concat_pp_p.
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i0 : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i0))
  (Core.cat_comp g (fwedge_in' I X i0))
i: I
ap f (pglue i) @ point_eq f = h i pt @ (ap g (pglue i) @ point_eq g)
        apply moveL_pM.
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i0 : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i0))
  (Core.cat_comp g (fwedge_in' I X i0))
i: I
(ap f (pglue i) @ point_eq f) @ (ap g (pglue i) @ point_eq g)^ = h i pt
        symmetry.
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i0 : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i0))
  (Core.cat_comp g (fwedge_in' I X i0))
i: I
h i pt = (ap f (pglue i) @ point_eq f) @ (ap g (pglue i) @ point_eq g)^
        exact (dpoint_eq (h i)).
    +
I: Type
X: I -> pType
Z: pType
f, g: Core.Hom (FamilyWedge I X) Z
h: forall i : I,
Core.GpdHom (Core.cat_comp f (fwedge_in' I X i))
  (Core.cat_comp g (fwedge_in' I X i))
Pushout_ind
  (fun w : Pushout (fun i : I => (i; pt)) (fun _ : I => pt) => f w = g w)
  (fun b : {x : I & X x} => (fun (i : I) (x : X i) => h i x) b.1 b.2)
  (fun c : pUnit =>
   match c as u return (f (pushr u) = g (pushr u)) with
   | tt => point_eq f @ (point_eq g)^
   end)
  (fun i : I =>
   transport_paths_FlFr (pglue i) (h i pt) @
   moveR_Vp_p_inv (ap f (pglue i)) (h i pt) (ap g (pglue i))
     (point_eq f @ (point_eq g)^)
     (concat_p_pp (ap f (pglue i)) (point_eq f) (point_eq g)^ @
      moveR_pV (point_eq g) (h i pt @ ap g (pglue i))
        (ap f (pglue i) @ point_eq f)
        (moveL_pM (ap g (pglue i) @ point_eq g) (ap f (pglue i) @ point_eq f)
           (h i pt) (dpoint_eq (h i))^ @
         (concat_pp_p (h i pt) (ap g (pglue i)) (point_eq g))^))
   :
   transport
     (fun w : Pushout (fun i0 : I => (i0; pt)) (fun _ : I => pt) => f w = g w)
     (pglue i)
     ((fun b : {x : I & X x} => (fun (i0 : I) (x : X i0) => h i0 x) b.1 b.2)
        ((fun i0 : I => (i0; pt)) i)) =
   (fun c : pUnit =>
    match c as u return (f (pushr u) = g (pushr u)) with
    | tt => point_eq f @ (point_eq g)^
    end) ((fun _ : I => pt) i))
  pt =
dpoint_eq f @ (dpoint_eq g)^ 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.
X: pType
psusp X ->* psusp X \/ psusp X
Proof.
X: pType
psusp X ->* psusp X \/ psusp X
  refine (Build_pMap (Susp_rec pt pt _) idpath).
X: pType
X -> pt = pt
  intros x.
X: pType
x: X
pt = pt
  refine (ap wedge_inl _ @ wglue @ ap wedge_inr _ @ wglue^).
X: pType
x: X
pt = pt
X: pType
x: X
pt = pt
  1,2: exact (loop_susp_unit X x).
Defined.

(** It should compute when [ap]ed 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^.
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.
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^
  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).
X: pType
wedge_pr1 o* psusp_pinch X ==* pmap_idmap
Proof.
X: pType
wedge_pr1 o* psusp_pinch X ==* pmap_idmap
  snapply Build_pHomotopy.
X: pType
wedge_pr1 o* psusp_pinch X == pmap_idmap
X: pType
?p pt = dpoint_eq (wedge_pr1 o* psusp_pinch X) @ (dpoint_eq pmap_idmap)^
  -
X: pType
wedge_pr1 o* psusp_pinch X == pmap_idmap snapply Susp_ind_FlFr.
X: pType
(wedge_pr1 o* psusp_pinch X) North = pmap_idmap North
X: pType
(wedge_pr1 o* psusp_pinch X) South = pmap_idmap South
X: pType
forall x : X,
ap (wedge_pr1 o* psusp_pinch X) (merid x) @ ?HS =
?HN @ ap pmap_idmap (merid x)
    +
X: pType
(wedge_pr1 o* psusp_pinch X) North = pmap_idmap North reflexivity.
    +
X: pType
(wedge_pr1 o* psusp_pinch X) South = pmap_idmap South exact (merid pt).
    +
X: pType
forall x : X,
ap (wedge_pr1 o* psusp_pinch X) (merid x) @ merid pt =
1 @ ap pmap_idmap (merid x) intros x.
X: pType
x: X
ap (wedge_pr1 o* psusp_pinch X) (merid x) @ merid pt =
1 @ ap pmap_idmap (merid x)
      rhs napply concat_1p.
X: pType
x: X
ap (wedge_pr1 o* psusp_pinch X) (merid x) @ merid pt =
ap pmap_idmap (merid x)
      rhs napply ap_idmap.
X: pType
x: X
ap (wedge_pr1 o* psusp_pinch X) (merid x) @ merid pt = merid x
      apply moveR_pM.
X: pType
x: X
ap (wedge_pr1 o* psusp_pinch X) (merid x) = merid x @ (merid pt)^
      change (?t = _) with (t = loop_susp_unit X x).
X: pType
x: X
ap (wedge_pr1 o* psusp_pinch X) (merid x) = loop_susp_unit X x
      lhs napply (ap_compose (psusp_pinch X)).
X: pType
x: X
ap wedge_pr1 (ap (psusp_pinch X) (merid x)) = loop_susp_unit X x
      lhs napply (ap _ (psusp_pinch_beta_merid x)).
X: pType
x: X
ap wedge_pr1
  (((ap wedge_inl (loop_susp_unit X x) @ wglue) @
    ap wedge_inr (loop_susp_unit X x)) @
   wglue^) =
loop_susp_unit X x
      lhs napply ap_pV.
X: pType
x: X
ap wedge_pr1
  ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
   ap wedge_inr (loop_susp_unit X x)) @
(ap wedge_pr1 wglue)^ = loop_susp_unit X x
      apply moveR_pV.
X: pType
x: X
ap wedge_pr1
  ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
   ap wedge_inr (loop_susp_unit X x)) =
loop_susp_unit X x @ ap wedge_pr1 wglue
      rhs napply (whiskerL _ (wedge_rec_beta_wglue _ _)).
X: pType
x: X
ap wedge_pr1
  ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
   ap wedge_inr (loop_susp_unit X x)) =
loop_susp_unit X x @ (point_eq pmap_idmap @ (point_eq pconst)^)
      lhs napply ap_pp.
X: pType
x: X
ap wedge_pr1 (ap wedge_inl (loop_susp_unit X x) @ wglue) @
ap wedge_pr1 (ap wedge_inr (loop_susp_unit X x)) =
loop_susp_unit X x @ (point_eq pmap_idmap @ (point_eq pconst)^)
      lhs napply (ap (fun x => _ @ x)).
X: pType
x: X
ap wedge_pr1 (ap wedge_inr (loop_susp_unit X x)) = ?Goal
X: pType
x: X
ap wedge_pr1 (ap wedge_inl (loop_susp_unit X x) @ wglue) @ ?Goal =
loop_susp_unit X x @ (point_eq pmap_idmap @ (point_eq pconst)^)
      {
X: pType
x: X
ap wedge_pr1 (ap wedge_inr (loop_susp_unit X x)) = ?Goal lhs_V napply ap_compose.
X: pType
x: X
ap (fun x0 : psusp X => wedge_pr1 (pushr x0)) (loop_susp_unit X x) = ?Goal
        apply ap_const. }
X: pType
x: X
ap wedge_pr1 (ap wedge_inl (loop_susp_unit X x) @ wglue) @ 1 =
loop_susp_unit X x @ (point_eq pmap_idmap @ (point_eq pconst)^)
      lhs napply concat_p1.
X: pType
x: X
ap wedge_pr1 (ap wedge_inl (loop_susp_unit X x) @ wglue) =
loop_susp_unit X x @ (point_eq pmap_idmap @ (point_eq pconst)^)
      lhs napply ap_pp.
X: pType
x: X
ap wedge_pr1 (ap wedge_inl (loop_susp_unit X x)) @ ap wedge_pr1 wglue =
loop_susp_unit X x @ (point_eq pmap_idmap @ (point_eq pconst)^)
      lhs napply (ap (fun x => _ @ x) (wedge_rec_beta_wglue _ _)).
X: pType
x: X
ap wedge_pr1 (ap wedge_inl (loop_susp_unit X x)) @
(point_eq pmap_idmap @ (point_eq pconst)^) =
loop_susp_unit X x @ (point_eq pmap_idmap @ (point_eq pconst)^)
      f_ap.
X: pType
x: X
ap wedge_pr1 (ap wedge_inl (loop_susp_unit X x)) = loop_susp_unit X x
      lhs_V napply (ap_compose wedge_inl).
X: pType
x: X
ap (fun x0 : psusp X => wedge_pr1 (wedge_inl x0)) (loop_susp_unit X x) =
loop_susp_unit X x
      apply ap_idmap.
  -
X: pType
Susp_ind_FlFr (wedge_pr1 o* psusp_pinch X) pmap_idmap 1 
  (merid pt)
  (fun x : X =>
   (moveR_pM (merid pt) (merid x) (ap (wedge_pr1 o* psusp_pinch X) (merid x))
      (ap_compose (psusp_pinch X) wedge_pr1 (merid x) @
       (ap (ap wedge_pr1) (psusp_pinch_beta_merid x) @
        (ap_pV wedge_pr1
           ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
            ap wedge_inr (loop_susp_unit X x))
           wglue @
         moveR_pV (ap wedge_pr1 wglue) (loop_susp_unit X x)
           (ap wedge_pr1
              ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
               ap wedge_inr (loop_susp_unit X x)))
           ((ap_pp wedge_pr1 (ap wedge_inl (loop_susp_unit X x) @ wglue)
               (ap wedge_inr (loop_susp_unit X x)) @
             (ap
                (fun x0 : wedge_pr1 (pushr pt) = wedge_pr1 (pushr pt) =>
                 ap wedge_pr1 (ap wedge_inl (loop_susp_unit X x) @ wglue) @
                 x0)
                ((ap_compose pushr wedge_pr1 (loop_susp_unit X x))^ @
                 ap_const (loop_susp_unit X x) (wedge_pr1 (pushr pt))) @
              (concat_p1
                 (ap wedge_pr1 (ap wedge_inl (loop_susp_unit X x) @ wglue)) @
               (ap_pp wedge_pr1 (ap wedge_inl (loop_susp_unit X x)) wglue @
                (ap
                   (fun
                      x0 : wedge_rec pmap_idmap pconst (pushl pt) =
                           wedge_rec pmap_idmap pconst (pushr pt) =>
                    ap wedge_pr1 (ap wedge_inl (loop_susp_unit X x)) @ x0)
                   (wedge_rec_beta_wglue pmap_idmap pconst) @
                 apD10
                   (ap11 1
                      ((ap_compose wedge_inl wedge_pr1 (loop_susp_unit X x))^ @
                       ap_idmap (loop_susp_unit X x)))
                   (point_eq pmap_idmap @ (point_eq pconst)^)))))) @
            (whiskerL (loop_susp_unit X x)
               (wedge_rec_beta_wglue pmap_idmap pconst))^)))) @
    (ap_idmap (merid x))^) @
   (concat_1p (ap pmap_idmap (merid x)))^)
  pt =
dpoint_eq (wedge_pr1 o* psusp_pinch X) @ (dpoint_eq pmap_idmap)^ reflexivity.
Defined.

Definition wedge_pr2_psusp_pinch {X}
  : wedge_pr2 o* psusp_pinch X ==* @pmap_idmap (psusp X).
X: pType
wedge_pr2 o* psusp_pinch X ==* pmap_idmap
Proof.
X: pType
wedge_pr2 o* psusp_pinch X ==* pmap_idmap
  snapply Build_pHomotopy.
X: pType
wedge_pr2 o* psusp_pinch X == pmap_idmap
X: pType
?p pt = dpoint_eq (wedge_pr2 o* psusp_pinch X) @ (dpoint_eq pmap_idmap)^
  -
X: pType
wedge_pr2 o* psusp_pinch X == pmap_idmap snapply Susp_ind_FlFr.
X: pType
(wedge_pr2 o* psusp_pinch X) North = pmap_idmap North
X: pType
(wedge_pr2 o* psusp_pinch X) South = pmap_idmap South
X: pType
forall x : X,
ap (wedge_pr2 o* psusp_pinch X) (merid x) @ ?HS =
?HN @ ap pmap_idmap (merid x)
    +
X: pType
(wedge_pr2 o* psusp_pinch X) North = pmap_idmap North reflexivity.
    +
X: pType
(wedge_pr2 o* psusp_pinch X) South = pmap_idmap South exact (merid pt).
    +
X: pType
forall x : X,
ap (wedge_pr2 o* psusp_pinch X) (merid x) @ merid pt =
1 @ ap pmap_idmap (merid x) intros x.
X: pType
x: X
ap (wedge_pr2 o* psusp_pinch X) (merid x) @ merid pt =
1 @ ap pmap_idmap (merid x)
      rhs napply concat_1p.
X: pType
x: X
ap (wedge_pr2 o* psusp_pinch X) (merid x) @ merid pt =
ap pmap_idmap (merid x)
      rhs napply ap_idmap.
X: pType
x: X
ap (wedge_pr2 o* psusp_pinch X) (merid x) @ merid pt = merid x
      apply moveR_pM.
X: pType
x: X
ap (wedge_pr2 o* psusp_pinch X) (merid x) = merid x @ (merid pt)^
      change (?t = _) with (t = loop_susp_unit X x).
X: pType
x: X
ap (wedge_pr2 o* psusp_pinch X) (merid x) = loop_susp_unit X x
      lhs napply (ap_compose (psusp_pinch X)).
X: pType
x: X
ap wedge_pr2 (ap (psusp_pinch X) (merid x)) = loop_susp_unit X x
      lhs napply (ap _ (psusp_pinch_beta_merid x)).
X: pType
x: X
ap wedge_pr2
  (((ap wedge_inl (loop_susp_unit X x) @ wglue) @
    ap wedge_inr (loop_susp_unit X x)) @
   wglue^) =
loop_susp_unit X x
      lhs napply ap_pV.
X: pType
x: X
ap wedge_pr2
  ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
   ap wedge_inr (loop_susp_unit X x)) @
(ap wedge_pr2 wglue)^ = loop_susp_unit X x
      apply moveR_pV.
X: pType
x: X
ap wedge_pr2
  ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
   ap wedge_inr (loop_susp_unit X x)) =
loop_susp_unit X x @ ap wedge_pr2 wglue
      rhs napply (whiskerL _ (wedge_rec_beta_wglue _ _)).
X: pType
x: X
ap wedge_pr2
  ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
   ap wedge_inr (loop_susp_unit X x)) =
loop_susp_unit X x @ (point_eq pconst @ (point_eq pmap_idmap)^)
      lhs napply ap_pp.
X: pType
x: X
ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x) @ wglue) @
ap wedge_pr2 (ap wedge_inr (loop_susp_unit X x)) =
loop_susp_unit X x @ (point_eq pconst @ (point_eq pmap_idmap)^)
      lhs napply (ap (fun x => _ @ x) _).
X: pType
x: X
ap wedge_pr2 (ap wedge_inr (loop_susp_unit X x)) = ?Goal
X: pType
x: X
ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x) @ wglue) @ ?Goal =
loop_susp_unit X x @ (point_eq pconst @ (point_eq pmap_idmap)^)
      {
X: pType
x: X
ap wedge_pr2 (ap wedge_inr (loop_susp_unit X x)) = ?Goal lhs_V napply ap_compose.
X: pType
x: X
ap (fun x0 : psusp X => wedge_pr2 (pushr x0)) (loop_susp_unit X x) = ?Goal
        apply ap_idmap. }
X: pType
x: X
ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x) @ wglue) @ loop_susp_unit X x =
loop_susp_unit X x @ (point_eq pconst @ (point_eq pmap_idmap)^)
      rhs napply concat_p1.
X: pType
x: X
ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x) @ wglue) @ loop_susp_unit X x =
loop_susp_unit X x
      apply moveR_pM.
X: pType
x: X
ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x) @ wglue) =
loop_susp_unit X x @ (loop_susp_unit X x)^
      lhs napply ap_pp.
X: pType
x: X
ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x)) @ ap wedge_pr2 wglue =
loop_susp_unit X x @ (loop_susp_unit X x)^
      rhs napply concat_pV.
X: pType
x: X
ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x)) @ ap wedge_pr2 wglue = 1
      lhs napply (ap _ (wedge_rec_beta_wglue _ _)).
X: pType
x: X
ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x)) @
(point_eq pconst @ (point_eq pmap_idmap)^) = 1
      apply moveR_pM.
X: pType
x: X
ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x)) =
1 @ (point_eq pconst @ (point_eq pmap_idmap)^)^
      lhs_V napply (ap_compose wedge_inl).
X: pType
x: X
ap (fun x0 : psusp X => wedge_pr2 (wedge_inl x0)) (loop_susp_unit X x) =
1 @ (point_eq pconst @ (point_eq pmap_idmap)^)^
      rapply ap_const.
  -
X: pType
Susp_ind_FlFr (wedge_pr2 o* psusp_pinch X) pmap_idmap 1 
  (merid pt)
  (fun x : X =>
   (moveR_pM (merid pt) (merid x) (ap (wedge_pr2 o* psusp_pinch X) (merid x))
      (ap_compose (psusp_pinch X) wedge_pr2 (merid x) @
       (ap (ap wedge_pr2) (psusp_pinch_beta_merid x) @
        (ap_pV wedge_pr2
           ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
            ap wedge_inr (loop_susp_unit X x))
           wglue @
         moveR_pV (ap wedge_pr2 wglue) (loop_susp_unit X x)
           (ap wedge_pr2
              ((ap wedge_inl (loop_susp_unit X x) @ wglue) @
               ap wedge_inr (loop_susp_unit X x)))
           ((ap_pp wedge_pr2 (ap wedge_inl (loop_susp_unit X x) @ wglue)
               (ap wedge_inr (loop_susp_unit X x)) @
             (ap
                (fun x0 : wedge_pr2 (pushr pt) = wedge_pr2 (pushr pt) =>
                 ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x) @ wglue) @
                 x0)
                ((ap_compose pushr wedge_pr2 (loop_susp_unit X x))^ @
                 ap_idmap (loop_susp_unit X x)) @
              (moveR_pM (loop_susp_unit X x) (loop_susp_unit X x)
                 (ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x) @ wglue))
                 (ap_pp wedge_pr2 (ap wedge_inl (loop_susp_unit X x)) wglue @
                  ((ap
                      (concat
                         (ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x))))
                      (wedge_rec_beta_wglue pconst pmap_idmap) @
                    moveR_pM (point_eq pconst @ (point_eq pmap_idmap)^) 1
                      (ap wedge_pr2 (ap wedge_inl (loop_susp_unit X x)))
                      ((ap_compose wedge_inl wedge_pr2 (loop_susp_unit X x))^ @
                       ap_const (loop_susp_unit X x)
                         (wedge_pr2 (wedge_inl pt)))) @
                   (concat_pV (loop_susp_unit X x))^)) @
               (concat_p1 (loop_susp_unit X x))^))) @
            (whiskerL (loop_susp_unit X x)
               (wedge_rec_beta_wglue pconst pmap_idmap))^)))) @
    (ap_idmap (merid x))^) @
   (concat_1p (ap pmap_idmap (merid x)))^)
  pt =
dpoint_eq (wedge_pr2 o* psusp_pinch X) @ (dpoint_eq pmap_idmap)^ reflexivity.
Defined.

(** ** Connectivity of wedge inclusion *)

Definition extension_wedge_incl {X Y : pType} (P : X * Y -> Type)
  (d : forall a : X \/ Y, P (wedge_incl X Y a))
  (f : forall (x : X) (y : Y), P (x, y))
  (p : forall (x : X), f x pt = d (wedge_inl x))
  (q : forall (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.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
ExtensionAlong (wedge_incl X Y) P d
Proof.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
ExtensionAlong (wedge_incl X Y) P d
  exists (prod_ind _ f).
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
forall x : X \/ Y, prod_ind P f (wedge_incl X Y x) = d x
  napply (wedge_ind _ p q).
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
transport (fun xy : X \/ Y => prod_ind P f (wedge_incl X Y xy) = d xy) wglue
  (p pt) =
q pt
  lhs napply (transport_paths_FlFr_D wglue).
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
((apD (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x)) wglue)^ @
 ap (transport (fun x : X \/ Y => P (wedge_incl X Y x)) wglue) (p pt)) @
apD d wglue = q pt
  apply moveR_pM.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
(apD (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x)) wglue)^ @
ap (transport (fun x : X \/ Y => P (wedge_incl X Y x)) wglue) (p pt) =
q pt @ (apD d wglue)^
  apply moveR_Vp.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
ap (transport (fun x : X \/ Y => P (wedge_incl X Y x)) wglue) (p pt) =
apD (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x)) wglue @
(q pt @ (apD d wglue)^)
  unshelve lhs napply ap_homotopic_id.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
forall x : P (wedge_incl X Y (pushr pt)),
transport (fun x0 : X \/ Y => P (wedge_incl X Y x0)) wglue x = x
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
(?Goal (prod_ind P f (wedge_incl X Y (pushl pt))) @ p pt) @
(?Goal (d (pushl pt)))^ =
apD (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x)) wglue @
(q pt @ (apD d wglue)^)
  1: exact (transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue).
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
(transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue
   (prod_ind P f (wedge_incl X Y (pushl pt))) @
 p pt) @
(transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue
   (d (pushl pt)))^ =
apD (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x)) wglue @
(q pt @ (apD d wglue)^)
  change (prod_ind P f (wedge_incl X Y (pushl pt))) with (f pt pt).
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
(transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue (f pt pt) @
 p pt) @
(transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue
   (d (pushl pt)))^ =
apD (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x)) wglue @
(q pt @ (apD d wglue)^)
  apply moveR_pV.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue (f pt pt) @
p pt =
(apD (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x)) wglue @
 (q pt @ (apD d wglue)^)) @
transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue
  (d (pushl pt))
  rhs napply concat_pp_p.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue (f pt pt) @
p pt =
apD (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x)) wglue @
((q pt @ (apD d wglue)^) @
 transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue
   (d (pushl pt)))
  rhs napply (1 @@ concat_pp_p _ _ _).
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue (f pt pt) @
p pt =
apD (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x)) wglue @
(q pt @
 ((apD d wglue)^ @
  transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue
    (d (pushl pt))))
  nrefine (_ @@ pq).
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue (f pt pt) =
apD (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x)) wglue
  symmetry.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
apD (fun x : X \/ Y => prod_ind P f (wedge_incl X Y x)) wglue =
transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue (f pt pt)
  lhs napply apD_compose.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
transport_compose P (wedge_incl X Y) wglue
  (prod_ind P f (wedge_incl X Y (pushl pt))) @
apD (prod_ind P f) (ap (wedge_incl X Y) wglue) =
transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue (f pt pt)
  unfold transport_compose_path_ap.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
transport_compose P (wedge_incl X Y) wglue
  (prod_ind P f (wedge_incl X Y (pushl pt))) @
apD (prod_ind P f) (ap (wedge_incl X Y) wglue) =
transport_compose P (wedge_incl X Y) wglue (f pt pt) @
transport2 P wedge_incl_beta_wglue (f pt pt)
  apply whiskerL.
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
apD (prod_ind P f) (ap (wedge_incl X Y) wglue) =
transport2 P wedge_incl_beta_wglue (f pt pt)
  lhs napply (apD02 _ wedge_incl_beta_wglue).
X, Y: pType
P: X * Y -> Type
d: forall a : X \/ Y, P (wedge_incl X Y a)
f: forall (x : X) (y : Y), P (x, y)
p: forall x : X, f x pt = d (wedge_inl x)
q: forall 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
   (d (pushl pt)))
transport2 P wedge_incl_beta_wglue (prod_ind P f (wedge_incl X Y (pushl pt))) @
apD (prod_ind P f) 1 = transport2 P wedge_incl_beta_wglue (f pt pt)
  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).
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
IsConnMap (Tr (m +2+ n)) (wedge_incl X Y)
Proof.
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
IsConnMap (Tr (m +2+ n)) (wedge_incl X Y)
  apply conn_map_from_extension_elim.
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
forall P : [X * Y, ispointed_prod] -> Type,
(forall b : [X * Y, ispointed_prod], In (Tr (m +2+ n)) (P b)) ->
forall d : forall a : X \/ Y, P (wedge_incl X Y a),
ExtensionAlong (wedge_incl X Y) P d
  intros P h d.
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod], In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
ExtensionAlong (wedge_incl X Y) P d
  snapply extension_wedge_incl.
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod], In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
forall (x : X) (y : Y), P (x, y)
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod], In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
forall x : X, ?f x pt = d (wedge_inl x)
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod], In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
forall y : Y, ?f pt y = d (wedge_inr y)
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod], In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
?p pt =
?q pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue
   (d (pushl pt)))
  -
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod], In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
forall (x : X) (y : Y), P (x, y) rapply (wedge_incl_elim _ _ (fun x y => P (x, y)) (d o wedge_inr) (d o wedge_inl)).
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod], In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
d (wedge_inr pt) = d (wedge_inl pt)
    lhs_V exact (apD d wglue).
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod], In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
transport (fun a : X \/ Y => P (wedge_incl X Y a)) wglue (d (pushl pt)) =
d (wedge_inl pt)
    exact (transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue _).
  -
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod], In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
forall x : X,
wedge_incl_elim pt pt (fun (x0 : X) (y : Y) => P (x0, y)) 
  (d o wedge_inr) (d o wedge_inl)
  ((apD d wglue)^ @
   transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue
     (d (pushl pt)))
  x pt =
d (wedge_inl x) napply wedge_incl_comp2.
  -
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod], In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
forall y : Y,
wedge_incl_elim pt pt (fun (x : X) (y0 : Y) => P (x, y0)) 
  (d o wedge_inr) (d o wedge_inl)
  ((apD d wglue)^ @
   transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue
     (d (pushl pt)))
  pt y =
d (wedge_inr y) napply wedge_incl_comp1.
  -
H: Univalence
m, n: trunc_index
X, Y: pType
IsConnected0: IsConnected (Tr m.+1) X
IsConnected1: IsConnected (Tr n.+1) Y
P: [X * Y, ispointed_prod] -> Type
h: forall b : [X * Y, ispointed_prod], In (Tr (m +2+ n)) (P b)
d: forall a : X \/ Y, P (wedge_incl X Y a)
wedge_incl_comp2 pt pt (fun (x : X) (y : Y) => P (x, y))
  (fun x : Y => d (wedge_inr x)) (fun x : X => d (wedge_inl x))
  ((apD d wglue)^ @
   transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue
     (d (pushl pt)))
  pt =
wedge_incl_comp1 pt pt (fun (x : X) (y : Y) => P (x, y))
  (fun x : Y => d (wedge_inr x)) (fun x : X => d (wedge_inl x))
  ((apD d wglue)^ @
   transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue
     (d (pushl pt)))
  pt @
((apD d wglue)^ @
 transport_compose_path_ap P (wedge_incl X Y) wedge_incl_beta_wglue
   (d (pushl pt))) napply wedge_incl_comp3.
Defined.

(** A more elementary fact is that a wedge of [n]-connected types is [n]-connected. *)
Definition isconnected_wedge `{Univalence} (n : trunc_index) (X Y : pType)
  `{IsConnected n X} `{IsConnected n Y}
  : IsConnected n (Wedge X Y).
H: Univalence
n: trunc_index
X, Y: pType
H0: IsConnected (Tr n) X
H1: IsConnected (Tr n) Y
IsConnected (Tr n) (X \/ Y)
Proof.
H: Univalence
n: trunc_index
X, Y: pType
H0: IsConnected (Tr n) X
H1: IsConnected (Tr n) Y
IsConnected (Tr n) (X \/ Y)
  destruct n.
H: Univalence
X, Y: pType
H0: IsConnected (Tr (-2)) X
H1: IsConnected (Tr (-2)) Y
IsConnected (Tr (-2)) (X \/ Y)
H: Univalence
n: trunc_index
X, Y: pType
H0: IsConnected (Tr n.+1) X
H1: IsConnected (Tr n.+1) Y
IsConnected (Tr n.+1) (X \/ Y)
  1: exact _.
H: Univalence
n: trunc_index
X, Y: pType
H0: IsConnected (Tr n.+1) X
H1: IsConnected (Tr n.+1) Y
IsConnected (Tr n.+1) (X \/ Y)
  apply isconnected_from_elim.
H: Univalence
n: trunc_index
X, Y: pType
H0: IsConnected (Tr n.+1) X
H1: IsConnected (Tr n.+1) Y
forall C : Type,
In (Tr n.+1) C -> forall f : X \/ Y -> C, NullHomotopy.NullHomotopy f
  intros C H' f.
H: Univalence
n: trunc_index
X, Y: pType
H0: IsConnected (Tr n.+1) X
H1: IsConnected (Tr n.+1) Y
C: Type
H': In (Tr n.+1) C
f: X \/ Y -> C
NullHomotopy.NullHomotopy f  exists (f pt).
H: Univalence
n: trunc_index
X, Y: pType
H0: IsConnected (Tr n.+1) X
H1: IsConnected (Tr n.+1) Y
C: Type
H': In (Tr n.+1) C
f: X \/ Y -> C
forall x : X \/ Y, f x = f pt
  intro x; symmetry; revert x.
H: Univalence
n: trunc_index
X, Y: pType
H0: IsConnected (Tr n.+1) X
H1: IsConnected (Tr n.+1) Y
C: Type
H': In (Tr n.+1) C
f: X \/ Y -> C
forall x : X \/ Y, f pt = f x
  snapply wedge_ind; cbn.
H: Univalence
n: trunc_index
X, Y: pType
H0: IsConnected (Tr n.+1) X
H1: IsConnected (Tr n.+1) Y
C: Type
H': In (Tr n.+1) C
f: X \/ Y -> C
forall x : X, f (pushl pt) = f (pushl x)
H: Univalence
n: trunc_index
X, Y: pType
H0: IsConnected (Tr n.+1) X
H1: IsConnected (Tr n.+1) Y
C: Type
H': In (Tr n.+1) C
f: X \/ Y -> C
forall y : Y, f (pushl pt) = f (pushr y)
H: Univalence
n: trunc_index
X, Y: pType
H0: IsConnected (Tr n.+1) X
H1: IsConnected (Tr n.+1) Y
C: Type
H': In (Tr n.+1) C
f: X \/ Y -> C
transport
  (fun xy : Pushout (unit_name pt) (unit_name pt) => f (pushl pt) = f xy)
  wglue (?Goal pt) =
?Goal0 pt
  -
H: Univalence
n: trunc_index
X, Y: pType
H0: IsConnected (Tr n.+1) X
H1: IsConnected (Tr n.+1) Y
C: Type
H': In (Tr n.+1) C
f: X \/ Y -> C
forall x : X, f (pushl pt) = f (pushl x) by rapply conn_point_elim.
  -
H: Univalence
n: trunc_index
X, Y: pType
H0: IsConnected (Tr n.+1) X
H1: IsConnected (Tr n.+1) Y
C: Type
H': In (Tr n.+1) C
f: X \/ Y -> C
forall y : Y, f (pushl pt) = f (pushr y) rapply conn_point_elim.
H: Univalence
n: trunc_index
X, Y: pType
H0: IsConnected (Tr n.+1) X
H1: IsConnected (Tr n.+1) Y
C: Type
H': In (Tr n.+1) C
f: X \/ Y -> C
f (pushl pt) = f (pushr pt)
    apply ap, wglue.
  -
H: Univalence
n: trunc_index
X, Y: pType
H0: IsConnected (Tr n.+1) X
H1: IsConnected (Tr n.+1) Y
C: Type
H': In (Tr n.+1) C
f: X \/ Y -> C
transport
  (fun xy : Pushout (unit_name pt) (unit_name pt) => f (pushl pt) = f xy)
  wglue (conn_point_elim n (fun a : X => f (pushl pt) = f (pushl a)) 1 pt) =
conn_point_elim n (fun a : Y => f (pushl pt) = f (pushr a)) (ap f wglue) pt transport_paths Fr.
H: Univalence
n: trunc_index
X, Y: pType
H0: IsConnected (Tr n.+1) X
H1: IsConnected (Tr n.+1) Y
C: Type
H': In (Tr n.+1) C
f: X \/ Y -> C
conn_point_elim n (fun a : X => f (pushl pt) = f (pushl a)) 1 pt @ ap f wglue =
conn_point_elim n (fun a : Y => f (pushl pt) = f (pushr a)) (ap f wglue) pt
    rewrite 2 conn_point_elim_comp.
H: Univalence
n: trunc_index
X, Y: pType
H0: IsConnected (Tr n.+1) X
H1: IsConnected (Tr n.+1) Y
C: Type
H': In (Tr n.+1) C
f: X \/ Y -> C
1 @ ap f wglue = ap f wglue
    apply concat_1p.
Defined.