Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.
Require Import Cubical.DPath Cubical.DPathSquare.
Require Import WildCat.
Require Import Colimits.Pushout.
Require Import Homotopy.NullHomotopy.
Require Import Truncations.Core.
Require Import Modalities.Modality.
Require Import Extensions.

(** * The suspension of a type *)

Generalizable Variables X A B f g n.

Local Open Scope path_scope.

(* ** Definition of suspension *)

(** We define the suspension of a type X as the pushout of 1 <- X -> 1 *)
Definition Susp (X : Type) := Pushout@{_ Set Set _} (const_tt X) (const_tt X).
Definition North {X} : Susp X := pushl tt.
Definition South {X} : Susp X := pushr tt.
Definition merid {X} (x : X) : North = South := pglue x.

(** We think of this as the HIT with two points [North] and [South] and a path [merid] between them *)

(** We can derive an induction principle for the suspension *)
Definition Susp_ind {X : Type} (P : Susp X -> Type)
  (H_N : P North) (H_S : P South)
  (H_merid : forall x:X, (merid x) # H_N = H_S)
  : forall (y : Susp X), P y.
X: Type
P: Susp X -> Type
H_N: P North
H_S: P South
H_merid: forall x : X,
transport P (merid x) H_N = H_S
forall y : Susp X, P y
Proof.
X: Type
P: Susp X -> Type
H_N: P North
H_S: P South
H_merid: forall x : X,
transport P (merid x) H_N = H_S
forall y : Susp X, P y
  srapply Pushout_ind.
X: Type
P: Susp X -> Type
H_N: P North
H_S: P South
H_merid: forall x : X,
transport P (merid x) H_N = H_S
forall b : Unit, P (pushl b)
X: Type
P: Susp X -> Type
H_N: P North
H_S: P South
H_merid: forall x : X,
transport P (merid x) H_N = H_S
forall c : Unit, P (pushr c)
X: Type
P: Susp X -> Type
H_N: P North
H_S: P South
H_merid: forall x : X,
transport P (merid x) H_N = H_S
forall a : X,
transport P (pglue a) (?pushb (const_tt X a)) =
?pushc (const_tt X a)
  -
X: Type
P: Susp X -> Type
H_N: P North
H_S: P South
H_merid: forall x : X,
transport P (merid x) H_N = H_S
forall b : Unit, P (pushl b) exact (Unit_ind H_N).
  -
X: Type
P: Susp X -> Type
H_N: P North
H_S: P South
H_merid: forall x : X,
transport P (merid x) H_N = H_S
forall c : Unit, P (pushr c) exact (Unit_ind H_S).
  -
X: Type
P: Susp X -> Type
H_N: P North
H_S: P South
H_merid: forall x : X,
transport P (merid x) H_N = H_S
forall a : X,
transport P (pglue a) (Unit_ind H_N (const_tt X a)) =
Unit_ind H_S (const_tt X a) exact (H_merid).
Defined.

(** We can also derive the computation rule *)
Definition Susp_ind_beta_merid {X : Type}
  (P : Susp X -> Type) (H_N : P North) (H_S : P South)
  (H_merid : forall x:X, (merid x) # H_N = H_S) (x : X)
  : apD (Susp_ind P H_N H_S H_merid) (merid x) = H_merid x.
X: Type
P: Susp X -> Type
H_N: P North
H_S: P South
H_merid: forall x : X,
transport P (merid x) H_N = H_S
x: X
apD (Susp_ind P H_N H_S H_merid) (merid x) = H_merid x
Proof.
X: Type
P: Susp X -> Type
H_N: P North
H_S: P South
H_merid: forall x : X,
transport P (merid x) H_N = H_S
x: X
apD (Susp_ind P H_N H_S H_merid) (merid x) = H_merid x
  srapply Pushout_ind_beta_pglue.
Defined.

(** We want to allow the user to forget that we've defined suspension as a pushout and make it look like it was defined directly as a HIT. This has the advantage of not having to assume any new HITs but allowing us to have conceptual clarity. *)
Arguments Susp : simpl never.
Arguments North : simpl never.
Arguments South : simpl never.
Arguments merid : simpl never.
Arguments Susp_ind_beta_merid : simpl never.

(** A version of [Susp_ind] specifically for proving that two functions defined on a suspension are homotopic. *)
Definition Susp_ind_FlFr {X Y : Type} (f g : Susp X -> Y)
  (HN : f North = g North)
  (HS : f South = g South)
  (Hmerid : forall x, ap f (merid x) @ HS = HN @ ap g (merid x))
  : f == g.
X, Y: Type
f, g: Susp X -> Y
HN: f North = g North
HS: f South = g South
Hmerid: forall x : X,
ap f (merid x) @ HS = HN @ ap g (merid x)
f == g
Proof.
X, Y: Type
f, g: Susp X -> Y
HN: f North = g North
HS: f South = g South
Hmerid: forall x : X,
ap f (merid x) @ HS = HN @ ap g (merid x)
f == g
  snapply (Susp_ind _ HN HS).
X, Y: Type
f, g: Susp X -> Y
HN: f North = g North
HS: f South = g South
Hmerid: forall x : X,
ap f (merid x) @ HS = HN @ ap g (merid x)
forall x : X,
transport (fun y : Susp X => f y = g y) (merid x) HN =
HS
  intros x.
X, Y: Type
f, g: Susp X -> Y
HN: f North = g North
HS: f South = g South
Hmerid: forall x : X,
ap f (merid x) @ HS = HN @ ap g (merid x)
x: X
transport (fun y : Susp X => f y = g y) (merid x) HN =
HS
  transport_paths FlFr.
X, Y: Type
f, g: Susp X -> Y
HN: f North = g North
HS: f South = g South
Hmerid: forall x : X,
ap f (merid x) @ HS = HN @ ap g (merid x)
x: X
ap f (merid x) @ HS = HN @ ap g (merid x)
  exact (Hmerid x).
Defined.

(** A version of [Susp_ind] specifically for proving that the composition of two functions to and from a suspension are homotopic to the identity map. *)
Definition Susp_ind_FFlr {X Y : Type} (f : Susp X -> Y) (g : Y -> Susp X)
  (HN : g (f North) = North)
  (HS : g (f South) = South)
  (Hmerid : forall x, ap g (ap f (merid x)) @ HS = HN @ merid x)
  : g o f == idmap.
X, Y: Type
f: Susp X -> Y
g: Y -> Susp X
HN: g (f North) = North
HS: g (f South) = South
Hmerid: forall x : X,
ap g (ap f (merid x)) @ HS = HN @ merid x
g o f == idmap
Proof.
X, Y: Type
f: Susp X -> Y
g: Y -> Susp X
HN: g (f North) = North
HS: g (f South) = South
Hmerid: forall x : X,
ap g (ap f (merid x)) @ HS = HN @ merid x
g o f == idmap
  snapply (Susp_ind _ HN HS).
X, Y: Type
f: Susp X -> Y
g: Y -> Susp X
HN: g (f North) = North
HS: g (f South) = South
Hmerid: forall x : X,
ap g (ap f (merid x)) @ HS = HN @ merid x
forall x : X,
transport (fun y : Susp X => (g o f) y = idmap y)
  (merid x) HN = HS
  intros x; cbn beta.
X, Y: Type
f: Susp X -> Y
g: Y -> Susp X
HN: g (f North) = North
HS: g (f South) = South
Hmerid: forall x : X,
ap g (ap f (merid x)) @ HS = HN @ merid x
x: X
transport (fun y : Susp X => g (f y) = y) (merid x) HN =
HS
  transport_paths FFlr.
X, Y: Type
f: Susp X -> Y
g: Y -> Susp X
HN: g (f North) = North
HS: g (f South) = South
Hmerid: forall x : X,
ap g (ap f (merid x)) @ HS = HN @ merid x
x: X
ap g (ap f (merid x)) @ HS = HN @ merid x
  exact (Hmerid x).
Defined.

Definition Susp_ind_FFlFr {X Y Z : Type}
  (f : Susp X -> Y) (g : Y -> Z) (h : Susp X -> Z)
  (HN : g (f North) = h North)
  (HS : g (f South) = h South)
  (Hmerid : forall x, ap g (ap f (merid x)) @ HS = HN @ ap h (merid x))
  : g o f == h.
X, Y, Z: Type
f: Susp X -> Y
g: Y -> Z
h: Susp X -> Z
HN: g (f North) = h North
HS: g (f South) = h South
Hmerid: forall x : X,
ap g (ap f (merid x)) @ HS =
HN @ ap h (merid x)
g o f == h
Proof.
X, Y, Z: Type
f: Susp X -> Y
g: Y -> Z
h: Susp X -> Z
HN: g (f North) = h North
HS: g (f South) = h South
Hmerid: forall x : X,
ap g (ap f (merid x)) @ HS =
HN @ ap h (merid x)
g o f == h
  snapply (Susp_ind _ HN HS).
X, Y, Z: Type
f: Susp X -> Y
g: Y -> Z
h: Susp X -> Z
HN: g (f North) = h North
HS: g (f South) = h South
Hmerid: forall x : X,
ap g (ap f (merid x)) @ HS =
HN @ ap h (merid x)
forall x : X,
transport (fun y : Susp X => (g o f) y = h y)
  (merid x) HN = HS
  intros x; cbn beta.
X, Y, Z: Type
f: Susp X -> Y
g: Y -> Z
h: Susp X -> Z
HN: g (f North) = h North
HS: g (f South) = h South
Hmerid: forall x : X,
ap g (ap f (merid x)) @ HS =
HN @ ap h (merid x)
x: X
transport (fun y : Susp X => g (f y) = h y) (merid x)
  HN = HS
  transport_paths FFlFr.
X, Y, Z: Type
f: Susp X -> Y
g: Y -> Z
h: Susp X -> Z
HN: g (f North) = h North
HS: g (f South) = h South
Hmerid: forall x : X,
ap g (ap f (merid x)) @ HS =
HN @ ap h (merid x)
x: X
ap g (ap f (merid x)) @ HS = HN @ ap h (merid x)
  exact (Hmerid x).
Defined.

(** A version of [Susp_ind] specifically for proving a composition square from a suspension. *)
Definition Susp_ind_FFlFFr {X Y Y' Z : Type}
  (f : Susp X -> Y) (f' : Susp X -> Y') (g : Y -> Z) (g' : Y' -> Z)
  (HN : g (f North) = g' (f' North)) (HS : g (f South) = g' (f' South))
  (Hmerid : forall x, ap g (ap f (merid x)) @ HS = HN @ ap g' (ap f' (merid x)))
  : g o f == g' o f'.
X, Y, Y', Z: Type
f: Susp X -> Y
f': Susp X -> Y'
g: Y -> Z
g': Y' -> Z
HN: g (f North) = g' (f' North)
HS: g (f South) = g' (f' South)
Hmerid: forall x : X,
ap g (ap f (merid x)) @ HS =
HN @ ap g' (ap f' (merid x))
g o f == g' o f'
Proof.
X, Y, Y', Z: Type
f: Susp X -> Y
f': Susp X -> Y'
g: Y -> Z
g': Y' -> Z
HN: g (f North) = g' (f' North)
HS: g (f South) = g' (f' South)
Hmerid: forall x : X,
ap g (ap f (merid x)) @ HS =
HN @ ap g' (ap f' (merid x))
g o f == g' o f'
  snapply (Susp_ind _ HN HS).
X, Y, Y', Z: Type
f: Susp X -> Y
f': Susp X -> Y'
g: Y -> Z
g': Y' -> Z
HN: g (f North) = g' (f' North)
HS: g (f South) = g' (f' South)
Hmerid: forall x : X,
ap g (ap f (merid x)) @ HS =
HN @ ap g' (ap f' (merid x))
forall x : X,
transport (fun y : Susp X => (g o f) y = (g' o f') y)
  (merid x) HN = HS
  intros x; cbn beta.
X, Y, Y', Z: Type
f: Susp X -> Y
f': Susp X -> Y'
g: Y -> Z
g': Y' -> Z
HN: g (f North) = g' (f' North)
HS: g (f South) = g' (f' South)
Hmerid: forall x : X,
ap g (ap f (merid x)) @ HS =
HN @ ap g' (ap f' (merid x))
x: X
transport (fun y : Susp X => g (f y) = g' (f' y))
  (merid x) HN = HS
  transport_paths FFlFFr.
X, Y, Y', Z: Type
f: Susp X -> Y
f': Susp X -> Y'
g: Y -> Z
g': Y' -> Z
HN: g (f North) = g' (f' North)
HS: g (f South) = g' (f' South)
Hmerid: forall x : X,
ap g (ap f (merid x)) @ HS =
HN @ ap g' (ap f' (merid x))
x: X
ap g (ap f (merid x)) @ HS =
HN @ ap g' (ap f' (merid x))
  exact (Hmerid x).
Defined.

(* ** Non-dependent eliminator. *)

Definition Susp_rec {X Y : Type}
  (H_N H_S : Y) (H_merid : X -> H_N = H_S)
  : Susp X -> Y
  := Pushout_rec (f:=const_tt X) (g:=const_tt X) Y (Unit_ind H_N) (Unit_ind H_S) H_merid.

Global Arguments Susp_rec {X Y}%_type_scope H_N H_S H_merid%_function_scope _.

Definition Susp_rec_beta_merid {X Y : Type}
  {H_N H_S : Y} {H_merid : X -> H_N = H_S} (x:X)
  : ap (Susp_rec H_N H_S H_merid) (merid x) = H_merid x.
X, Y: Type
H_N, H_S: Y
H_merid: X -> H_N = H_S
x: X
ap (Susp_rec H_N H_S H_merid) (merid x) = H_merid x
Proof.
X, Y: Type
H_N, H_S: Y
H_merid: X -> H_N = H_S
x: X
ap (Susp_rec H_N H_S H_merid) (merid x) = H_merid x
  srapply Pushout_rec_beta_pglue.
Defined.

Definition Susp_rec_beta_zigzag {X Y : Type}
  {H_N H_S : Y} {H_merid : X -> H_N = H_S} (x x' : X)
  : ap (Susp_rec H_N H_S H_merid) (merid x @ (merid x')^) = H_merid x @ (H_merid x')^.
X, Y: Type
H_N, H_S: Y
H_merid: X -> H_N = H_S
x, x': X
ap (Susp_rec H_N H_S H_merid) (merid x @ (merid x')^) =
H_merid x @ (H_merid x')^
Proof.
X, Y: Type
H_N, H_S: Y
H_merid: X -> H_N = H_S
x, x': X
ap (Susp_rec H_N H_S H_merid) (merid x @ (merid x')^) =
H_merid x @ (H_merid x')^
  lhs napply ap_pV.
X, Y: Type
H_N, H_S: Y
H_merid: X -> H_N = H_S
x, x': X
ap (Susp_rec H_N H_S H_merid) (merid x) @
(ap (Susp_rec H_N H_S H_merid) (merid x'))^ =
H_merid x @ (H_merid x')^
  exact (Susp_rec_beta_merid x @@ inverse2 (Susp_rec_beta_merid x')).
Defined.

(** A variant of [Susp_ind_FlFr] specifically for two functions both defined using [Susp_rec]. *)
Definition Susp_rec_homotopic {X Y : Type} (N S N' S' : Y)
  (f : X -> N = S) (f' : X -> N' = S')
  (p : N = N') (q : S = S') (H : forall x, f x @ q = p @ f' x)
  : Susp_rec N S f == Susp_rec N' S' f'.
X, Y: Type
N, S, N', S': Y
f: X -> N = S
f': X -> N' = S'
p: N = N'
q: S = S'
H: forall x : X, f x @ q = p @ f' x
Susp_rec N S f == Susp_rec N' S' f'
Proof.
X, Y: Type
N, S, N', S': Y
f: X -> N = S
f': X -> N' = S'
p: N = N'
q: S = S'
H: forall x : X, f x @ q = p @ f' x
Susp_rec N S f == Susp_rec N' S' f'
  snapply Susp_ind_FlFr.
X, Y: Type
N, S, N', S': Y
f: X -> N = S
f': X -> N' = S'
p: N = N'
q: S = S'
H: forall x : X, f x @ q = p @ f' x
Susp_rec N S f North = Susp_rec N' S' f' North
X, Y: Type
N, S, N', S': Y
f: X -> N = S
f': X -> N' = S'
p: N = N'
q: S = S'
H: forall x : X, f x @ q = p @ f' x
Susp_rec N S f South = Susp_rec N' S' f' South
X, Y: Type
N, S, N', S': Y
f: X -> N = S
f': X -> N' = S'
p: N = N'
q: S = S'
H: forall x : X, f x @ q = p @ f' x
forall x : X,
ap (Susp_rec N S f) (merid x) @ ?HS =
?HN @ ap (Susp_rec N' S' f') (merid x)
  -
X, Y: Type
N, S, N', S': Y
f: X -> N = S
f': X -> N' = S'
p: N = N'
q: S = S'
H: forall x : X, f x @ q = p @ f' x
Susp_rec N S f North = Susp_rec N' S' f' North exact p.
  -
X, Y: Type
N, S, N', S': Y
f: X -> N = S
f': X -> N' = S'
p: N = N'
q: S = S'
H: forall x : X, f x @ q = p @ f' x
Susp_rec N S f South = Susp_rec N' S' f' South exact q.
  -
X, Y: Type
N, S, N', S': Y
f: X -> N = S
f': X -> N' = S'
p: N = N'
q: S = S'
H: forall x : X, f x @ q = p @ f' x
forall x : X,
ap (Susp_rec N S f) (merid x) @ q =
p @ ap (Susp_rec N' S' f') (merid x) intro x.
X, Y: Type
N, S, N', S': Y
f: X -> N = S
f': X -> N' = S'
p: N = N'
q: S = S'
H: forall x : X, f x @ q = p @ f' x
x: X
ap (Susp_rec N S f) (merid x) @ q =
p @ ap (Susp_rec N' S' f') (merid x)
    lhs napply (Susp_rec_beta_merid x @@ 1).
X, Y: Type
N, S, N', S': Y
f: X -> N = S
f': X -> N' = S'
p: N = N'
q: S = S'
H: forall x : X, f x @ q = p @ f' x
x: X
f x @ q = p @ ap (Susp_rec N' S' f') (merid x)
    rhs napply (1 @@ Susp_rec_beta_merid x).
X, Y: Type
N, S, N', S': Y
f: X -> N = S
f': X -> N' = S'
p: N = N'
q: S = S'
H: forall x : X, f x @ q = p @ f' x
x: X
f x @ q = p @ f' x
    apply H.
Defined.

(** And the special case where the two functions agree definitionally on [North] and [South]. *)
Definition Susp_rec_homotopic' {X Y : Type} (N S : Y)
  (f g : X -> N = S) (H : f == g)
  : Susp_rec N S f == Susp_rec N S g.
X, Y: Type
N, S: Y
f, g: X -> N = S
H: f == g
Susp_rec N S f == Susp_rec N S g
Proof.
X, Y: Type
N, S: Y
f, g: X -> N = S
H: f == g
Susp_rec N S f == Susp_rec N S g
  snapply Susp_rec_homotopic.
X, Y: Type
N, S: Y
f, g: X -> N = S
H: f == g
N = N
X, Y: Type
N, S: Y
f, g: X -> N = S
H: f == g
S = S
X, Y: Type
N, S: Y
f, g: X -> N = S
H: f == g
forall x : X, f x @ ?q = ?p @ g x
  1, 2: reflexivity.
X, Y: Type
N, S: Y
f, g: X -> N = S
H: f == g
forall x : X, f x @ 1 = 1 @ g x
  intro x; apply equiv_p1_1q, H.
Defined.

(** ** Eta-rule. *)

(** The eta-rule for suspension states that any function out of a suspension is equal to one defined by [Susp_ind] in the obvious way. We give it first in a weak form, producing just a pointwise equality, and then turn this into an actual equality using [Funext]. *)
Definition Susp_ind_eta_homotopic {X : Type} {P : Susp X -> Type} (f : forall y, P y)
  : f == Susp_ind P (f North) (f South) (fun x => apD f (merid x)).
X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
f ==
Susp_ind P (f North) (f South)
  (fun x : X => apD f (merid x))
Proof.
X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
f ==
Susp_ind P (f North) (f South)
  (fun x : X => apD f (merid x))
  unfold pointwise_paths.
X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
forall x : Susp X,
f x =
Susp_ind P (f North) (f South)
  (fun x0 : X => apD f (merid x0)) x refine (Susp_ind _ 1 1 _).
X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
forall x : X,
transport
  (fun y : Susp X =>
   f y =
   Susp_ind P (f North) (f South)
     (fun x0 : X => apD f (merid x0)) y) (merid x) 1 =
1
  intros x.
X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
x: X
transport
  (fun y : Susp X =>
   f y =
   Susp_ind P (f North) (f South)
     (fun x : X => apD f (merid x)) y) (merid x) 1 = 1
  refine (transport_paths_FlFr_D
    (g := Susp_ind P (f North) (f South) (fun x : X => apD f (merid x)))
    _ _ @ _); simpl.
X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
x: X
((apD f (merid x))^ @ 1) @
apD
  (Susp_ind P (f North) (f South)
     (fun x : X => apD f (merid x))) (merid x) = 1
  apply moveR_pM.
X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
x: X
(apD f (merid x))^ @ 1 =
1 @
(apD
   (Susp_ind P (f North) (f South)
      (fun x : X => apD f (merid x))) (merid x))^
  apply equiv_p1_1q.
X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
x: X
(apD f (merid x))^ =
(apD
   (Susp_ind P (f North) (f South)
      (fun x : X => apD f (merid x))) (merid x))^
  apply ap, inverse.
X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
x: X
apD
  (Susp_ind P (f North) (f South)
     (fun x : X => apD f (merid x))) (merid x) =
apD f (merid x) exact (Susp_ind_beta_merid _ _ _ _ _).
Defined.

Definition Susp_rec_eta_homotopic {X Y : Type} (f : Susp X -> Y)
  : f == Susp_rec (f North) (f South) (fun x => ap f (merid x)).
X, Y: Type
f: Susp X -> Y
f ==
Susp_rec (f North) (f South)
  (fun x : X => ap f (merid x))
Proof.
X, Y: Type
f: Susp X -> Y
f ==
Susp_rec (f North) (f South)
  (fun x : X => ap f (merid x))
  snapply Susp_ind_FlFr.
X, Y: Type
f: Susp X -> Y
f North =
Susp_rec (f North) (f South)
  (fun x : X => ap f (merid x)) North
X, Y: Type
f: Susp X -> Y
f South =
Susp_rec (f North) (f South)
  (fun x : X => ap f (merid x)) South
X, Y: Type
f: Susp X -> Y
forall x : X,
ap f (merid x) @ ?HS =
?HN @
ap
  (Susp_rec (f North) (f South)
     (fun x0 : X => ap f (merid x0))) (merid x)
  1, 2: reflexivity.
X, Y: Type
f: Susp X -> Y
forall x : X,
ap f (merid x) @ 1 =
1 @
ap
  (Susp_rec (f North) (f South)
     (fun x0 : X => ap f (merid x0))) (merid x)
  intro x.
X, Y: Type
f: Susp X -> Y
x: X
ap f (merid x) @ 1 =
1 @
ap
  (Susp_rec (f North) (f South)
     (fun x : X => ap f (merid x))) (merid x)
  apply equiv_p1_1q.
X, Y: Type
f: Susp X -> Y
x: X
ap f (merid x) =
ap
  (Susp_rec (f North) (f South)
     (fun x : X => ap f (merid x))) (merid x)
  exact (Susp_rec_beta_merid _)^.
Defined.

Definition Susp_ind_eta `{Funext}
  {X : Type} {P : Susp X -> Type} (f : forall y, P y)
  : f = Susp_ind P (f North) (f South) (fun x => apD f (merid x))
  := path_forall _ _ (Susp_ind_eta_homotopic f).

Definition Susp_rec_eta `{Funext} {X Y : Type} (f : Susp X -> Y)
  : f = Susp_rec (f North) (f South) (fun x => ap f (merid x))
  := path_forall _ _ (Susp_rec_eta_homotopic f).

(** ** Functoriality *)

Definition functor_susp {X Y : Type} (f : X -> Y)
  : Susp X -> Susp Y.
X, Y: Type
f: X -> Y
Susp X -> Susp Y
Proof.
X, Y: Type
f: X -> Y
Susp X -> Susp Y
  srapply Susp_rec.
X, Y: Type
f: X -> Y
Susp Y
X, Y: Type
f: X -> Y
Susp Y
X, Y: Type
f: X -> Y
X -> ?H_N = ?H_S
  -
X, Y: Type
f: X -> Y
Susp Y exact North.
  -
X, Y: Type
f: X -> Y
Susp Y exact South.
  -
X, Y: Type
f: X -> Y
X -> North = South intros x; exact (merid (f x)).
Defined.

Definition functor_susp_beta_merid {X Y : Type} (f : X -> Y) (x : X)
  : ap (functor_susp f) (merid x) = merid (f x).
X, Y: Type
f: X -> Y
x: X
ap (functor_susp f) (merid x) = merid (f x)
Proof.
X, Y: Type
f: X -> Y
x: X
ap (functor_susp f) (merid x) = merid (f x)
  srapply Susp_rec_beta_merid.
Defined.

Definition functor_susp_compose {X Y Z}
  (f : X -> Y) (g : Y -> Z)
  : functor_susp (g o f) == functor_susp g o functor_susp f.
X, Y, Z: Type
f: X -> Y
g: Y -> Z
functor_susp (g o f) ==
functor_susp g o functor_susp f
Proof.
X, Y, Z: Type
f: X -> Y
g: Y -> Z
functor_susp (g o f) ==
functor_susp g o functor_susp f
  snapply Susp_ind_FlFr.
X, Y, Z: Type
f: X -> Y
g: Y -> Z
functor_susp (g o f) North =
(fun x : Susp X => functor_susp g (functor_susp f x))
  North
X, Y, Z: Type
f: X -> Y
g: Y -> Z
functor_susp (g o f) South =
(fun x : Susp X => functor_susp g (functor_susp f x))
  South
X, Y, Z: Type
f: X -> Y
g: Y -> Z
forall x : X,
ap (functor_susp (g o f)) (merid x) @ ?HS =
?HN @
ap
  (fun x0 : Susp X =>
   functor_susp g (functor_susp f x0)) (merid x)
  1,2: reflexivity.
X, Y, Z: Type
f: X -> Y
g: Y -> Z
forall x : X,
ap (functor_susp (g o f)) (merid x) @ 1 =
1 @
ap
  (fun x0 : Susp X =>
   functor_susp g (functor_susp f x0)) (merid x)
  intro x.
X, Y, Z: Type
f: X -> Y
g: Y -> Z
x: X
ap (functor_susp (g o f)) (merid x) @ 1 =
1 @
ap
  (fun x : Susp X => functor_susp g (functor_susp f x))
  (merid x)
  apply equiv_p1_1q.
X, Y, Z: Type
f: X -> Y
g: Y -> Z
x: X
ap (functor_susp (fun x : X => g (f x))) (merid x) =
ap
  (fun x : Susp X => functor_susp g (functor_susp f x))
  (merid x)
  lhs napply functor_susp_beta_merid; symmetry.
X, Y, Z: Type
f: X -> Y
g: Y -> Z
x: X
ap
  (fun x : Susp X => functor_susp g (functor_susp f x))
  (merid x) = merid (g (f x))
  lhs nrefine (ap_compose (functor_susp f) _ (merid x)).
X, Y, Z: Type
f: X -> Y
g: Y -> Z
x: X
ap (functor_susp g) (ap (functor_susp f) (merid x)) =
merid (g (f x))
  lhs nrefine (ap _ (functor_susp_beta_merid _ _)).
X, Y, Z: Type
f: X -> Y
g: Y -> Z
x: X
ap (functor_susp g) (merid (f x)) = merid (g (f x))
  apply functor_susp_beta_merid.
Defined.

Definition functor_susp_idmap {X}
  : functor_susp idmap == (idmap : Susp X -> Susp X).
X: Type
functor_susp idmap == (idmap : Susp X -> Susp X)
Proof.
X: Type
functor_susp idmap == (idmap : Susp X -> Susp X)
  snapply Susp_ind_FlFr.
X: Type
functor_susp idmap North = idmap North
X: Type
functor_susp idmap South = idmap South
X: Type
forall x : X,
ap (functor_susp idmap) (merid x) @ ?HS =
?HN @ ap idmap (merid x)
  1,2: reflexivity.
X: Type
forall x : X,
ap (functor_susp idmap) (merid x) @ 1 =
1 @ ap idmap (merid x)
  intro x.
X: Type
x: X
ap (functor_susp idmap) (merid x) @ 1 =
1 @ ap idmap (merid x)
  apply equiv_p1_1q.
X: Type
x: X
ap (functor_susp idmap) (merid x) = ap idmap (merid x)
  lhs napply functor_susp_beta_merid.
X: Type
x: X
merid x = ap idmap (merid x)
  symmetry; apply ap_idmap.
Defined.

Definition functor2_susp {X Y} {f g : X -> Y} (h : f == g)
  : functor_susp f == functor_susp g.
X, Y: Type
f, g: X -> Y
h: f == g
functor_susp f == functor_susp g
Proof.
X, Y: Type
f, g: X -> Y
h: f == g
functor_susp f == functor_susp g
  srapply Susp_ind_FlFr.
X, Y: Type
f, g: X -> Y
h: f == g
functor_susp f North = functor_susp g North
X, Y: Type
f, g: X -> Y
h: f == g
functor_susp f South = functor_susp g South
X, Y: Type
f, g: X -> Y
h: f == g
forall x : X,
ap (functor_susp f) (merid x) @ ?HS =
?HN @ ap (functor_susp g) (merid x)
  1, 2: reflexivity.
X, Y: Type
f, g: X -> Y
h: f == g
forall x : X,
ap (functor_susp f) (merid x) @ 1 =
1 @ ap (functor_susp g) (merid x)
  intro x.
X, Y: Type
f, g: X -> Y
h: f == g
x: X
ap (functor_susp f) (merid x) @ 1 =
1 @ ap (functor_susp g) (merid x)
  apply equiv_p1_1q.
X, Y: Type
f, g: X -> Y
h: f == g
x: X
ap (functor_susp f) (merid x) =
ap (functor_susp g) (merid x)
  lhs napply (functor_susp_beta_merid f).
X, Y: Type
f, g: X -> Y
h: f == g
x: X
merid (f x) = ap (functor_susp g) (merid x)
  rhs napply (functor_susp_beta_merid g).
X, Y: Type
f, g: X -> Y
h: f == g
x: X
merid (f x) = merid (g x)
  apply ap, h.
Defined.

Instance is0functor_susp : Is0Functor Susp
  := Build_Is0Functor _ _ _ _ Susp (@functor_susp).

Instance is1functor_susp : Is1Functor Susp
  := Build_Is1Functor _ _ _ _ _ _ _ _ _ _ Susp _
      (@functor2_susp) (@functor_susp_idmap) (@functor_susp_compose).

(** ** Universal property *)

Definition equiv_Susp_rec `{Funext} (X Y : Type)
  : (Susp X -> Y) <~> { NS : Y * Y & X -> fst NS = snd NS }.
H: Funext
X, Y: Type
(Susp X -> Y) <~> {NS : Y * Y & X -> fst NS = snd NS}
Proof.
H: Funext
X, Y: Type
(Susp X -> Y) <~> {NS : Y * Y & X -> fst NS = snd NS}
  snapply equiv_adjointify.
H: Funext
X, Y: Type
(Susp X -> Y) -> {NS : Y * Y & X -> fst NS = snd NS}
H: Funext
X, Y: Type
{NS : Y * Y & X -> fst NS = snd NS} -> Susp X -> Y
H: Funext
X, Y: Type
?f o ?g == idmap
H: Funext
X, Y: Type
?g o ?f == idmap
  -
H: Funext
X, Y: Type
(Susp X -> Y) -> {NS : Y * Y & X -> fst NS = snd NS} intros f.
H: Funext
X, Y: Type
f: Susp X -> Y
{NS : Y * Y & X -> fst NS = snd NS}
    exists (f North, f South).
H: Funext
X, Y: Type
f: Susp X -> Y
X -> fst (f North, f South) = snd (f North, f South)
    intros x; exact (ap f (merid x)).
  -
H: Funext
X, Y: Type
{NS : Y * Y & X -> fst NS = snd NS} -> Susp X -> Y intros [[N S] m].
H: Funext
X, Y: Type
N, S: Y
m: X -> fst (N, S) = snd (N, S)
Susp X -> Y
    exact (Susp_rec N S m).
  -
H: Funext
X, Y: Type
(fun f : Susp X -> Y =>
 ((f North, f South); fun x : X => ap f (merid x)))
o (fun X0 : {NS : Y * Y & X -> fst NS = snd NS} =>
   (fun proj1 : Y * Y =>
    (fun (N S : Y) (m : X -> fst (N, S) = snd (N, S))
     => Susp_rec N S m) (fst proj1) (snd proj1)) X0.1
     X0.2) == idmap intros [[N S] m].
H: Funext
X, Y: Type
N, S: Y
m: X -> fst (N, S) = snd (N, S)
((Susp_rec N S m North, Susp_rec N S m South);
fun x : X => ap (Susp_rec N S m) (merid x)) =
((N, S); m)
    apply ap, path_arrow.
H: Funext
X, Y: Type
N, S: Y
m: X -> fst (N, S) = snd (N, S)
(fun x : X => ap (Susp_rec N S m) (merid x)) == m
    intros x; apply Susp_rec_beta_merid.
  -
H: Funext
X, Y: Type
(fun X0 : {NS : Y * Y & X -> fst NS = snd NS} =>
 (fun proj1 : Y * Y =>
  (fun (N S : Y) (m : X -> fst (N, S) = snd (N, S)) =>
   Susp_rec N S m) (fst proj1) (snd proj1)) X0.1 X0.2)
o (fun f : Susp X -> Y =>
   ((f North, f South); fun x : X => ap f (merid x))) ==
idmap intros f.
H: Funext
X, Y: Type
f: Susp X -> Y
Susp_rec (f North) (f South)
  (fun x : X => ap f (merid x)) = f
    symmetry; apply Susp_rec_eta.
Defined.

(** Using wild 0-groupoids, the universal property can be proven without funext.  A simple equivalence of 0-groupoids between [Susp X -> Y] and [{ NS : Y * Y & X -> fst NS = snd NS }] would not carry all the higher-dimensional information, but if we generalize it to dependent functions, then it does suffice. *)
Section UnivProp.
  Context (X : Type) (P : Susp X -> Type).

  (** Here is the domain of the equivalence: sections of [P] over [Susp X]. *)
  Definition Susp_ind_type := forall z:Susp X, P z.

  (** [isgraph_paths] is not a global instance, so we define this by hand.  The fact that this is a 01cat and a 0gpd is obtained using global instances. *)
  Local Instance isgraph_Susp_ind_type : IsGraph Susp_ind_type.
X: Type
P: Susp X -> Type
IsGraph Susp_ind_type
  Proof.
X: Type
P: Susp X -> Type
IsGraph Susp_ind_type apply isgraph_forall; intros; apply isgraph_paths. Defined.

  (** The codomain is a sigma-groupoid of this family, consisting of input data for [Susp_ind]. *)
  Definition Susp_ind_data' (NS : P North * P South)
    := forall x:X, DPath P (merid x) (fst NS) (snd NS).

  (** Again, the rest of the wild category structure is obtained using global instances. *)
  Local Instance isgraph_Susp_ind_data' NS : IsGraph (Susp_ind_data' NS).
X: Type
P: Susp X -> Type
NS: P North * P South
IsGraph (Susp_ind_data' NS)
  Proof.
X: Type
P: Susp X -> Type
NS: P North * P South
IsGraph (Susp_ind_data' NS) apply isgraph_forall; intros; apply isgraph_paths. Defined.

  (** Here is the codomain itself.  This is a 01cat and a 0gpd via global instances. *)
  Definition Susp_ind_data := sig Susp_ind_data'.

  (** Here is the functor. *)
  Definition Susp_ind_inv : Susp_ind_type -> Susp_ind_data.
X: Type
P: Susp X -> Type
Susp_ind_type -> Susp_ind_data
  Proof.
X: Type
P: Susp X -> Type
Susp_ind_type -> Susp_ind_data
    intros f.
X: Type
P: Susp X -> Type
f: Susp_ind_type
Susp_ind_data
    exists (f North,f South).
X: Type
P: Susp X -> Type
f: Susp_ind_type
Susp_ind_data' (f North, f South)
    intros x.
X: Type
P: Susp X -> Type
f: Susp_ind_type
x: X
DPath P (merid x) (fst (f North, f South))
  (snd (f North, f South))
    exact (apD f (merid x)).
  Defined.

  Local Instance is0functor_susp_ind_inv : Is0Functor Susp_ind_inv.
X: Type
P: Susp X -> Type
Is0Functor Susp_ind_inv
  Proof.
X: Type
P: Susp X -> Type
Is0Functor Susp_ind_inv
    constructor; unfold Susp_ind_type; cbn.
X: Type
P: Susp X -> Type
forall a b : forall z : Susp X, P z,
(forall a0 : Susp X, a a0 = b a0) ->
{p : (a North, a South) = (b North, b South) &
forall a0 : X,
transport Susp_ind_data' p
  (fun x : X => apD a (merid x)) a0 = apD b (merid a0)}
    intros f g p.
X: Type
P: Susp X -> Type
f, g: forall z : Susp X, P z
p: forall a : Susp X, f a = g a
{p : (f North, f South) = (g North, g South) &
forall a : X,
transport Susp_ind_data' p
  (fun x : X => apD f (merid x)) a = apD g (merid a)}
    unshelve econstructor.
X: Type
P: Susp X -> Type
f, g: forall z : Susp X, P z
p: forall a : Susp X, f a = g a
(f North, f South) = (g North, g South)
X: Type
P: Susp X -> Type
f, g: forall z : Susp X, P z
p: forall a : Susp X, f a = g a
forall a : X,
transport Susp_ind_data' ?p
  (fun x : X => apD f (merid x)) a = apD g (merid a)
    -
X: Type
P: Susp X -> Type
f, g: forall z : Susp X, P z
p: forall a : Susp X, f a = g a
(f North, f South) = (g North, g South) apply path_prod; apply p.
    -
X: Type
P: Susp X -> Type
f, g: forall z : Susp X, P z
p: forall a : Susp X, f a = g a
forall a : X,
transport Susp_ind_data'
  (path_prod (f North, f South) (g North, g South)
     (p North) (p South))
  (fun x : X => apD f (merid x)) a = apD g (merid a) intros x.
X: Type
P: Susp X -> Type
f, g: forall z : Susp X, P z
p: forall a : Susp X, f a = g a
x: X
transport Susp_ind_data'
  (path_prod (f North, f South) (g North, g South)
     (p North) (p South))
  (fun x : X => apD f (merid x)) x = apD g (merid x)
      rewrite transport_path_prod, !transport_forall_constant; cbn.
X: Type
P: Susp X -> Type
f, g: forall z : Susp X, P z
p: forall a : Susp X, f a = g a
x: X
transport
  (fun x0 : P North =>
   transport P (merid x) x0 = g South) (p North)
  (transport
     (fun x0 : P South =>
      transport P (merid x) (f North) = x0) (p South)
     (apD f (merid x))) = apD g (merid x)
      apply ds_transport_dpath.
X: Type
P: Susp X -> Type
f, g: forall z : Susp X, P z
p: forall a : Susp X, f a = g a
x: X
DPathSquare P (PathSquare.sq_refl_h (merid x))
  (apD f (merid x)) (apD g (merid x)) (p North)
  (p South)
      exact (dp_apD_nat p (merid x)).
  Defined.

  (** And now we can prove that it's an equivalence of 0-groupoids, using the definition from WildCat/EquivGpd. *)
  Definition issurjinj_Susp_ind_inv : IsSurjInj Susp_ind_inv.
X: Type
P: Susp X -> Type
IsSurjInj Susp_ind_inv
  Proof.
X: Type
P: Susp X -> Type
IsSurjInj Susp_ind_inv
    constructor.
X: Type
P: Susp X -> Type
SplEssSurj Susp_ind_inv
X: Type
P: Susp X -> Type
forall x y : Susp_ind_type,
Susp_ind_inv x $== Susp_ind_inv y -> x $== y
    -
X: Type
P: Susp X -> Type
SplEssSurj Susp_ind_inv intros [[n s] g].
X: Type
P: Susp X -> Type
n: P North
s: P South
g: Susp_ind_data' (n, s)
{a : Susp_ind_type & Susp_ind_inv a $== ((n, s); g)}
      exists (Susp_ind P n s g); cbn.
X: Type
P: Susp X -> Type
n: P North
s: P South
g: Susp_ind_data' (n, s)
{p
: (Susp_ind P n s g North, Susp_ind P n s g South) =
  (n, s) &
forall a : X,
transport Susp_ind_data' p
  (fun x : X => apD (Susp_ind P n s g) (merid x)) a =
g a}
      exists idpath.
X: Type
P: Susp X -> Type
n: P North
s: P South
g: Susp_ind_data' (n, s)
forall a : X,
transport Susp_ind_data' 1
  (fun x : X => apD (Susp_ind P n s g) (merid x)) a =
g a
      intros x; cbn.
X: Type
P: Susp X -> Type
n: P North
s: P South
g: Susp_ind_data' (n, s)
x: X
apD (Susp_ind P n s g) (merid x) = g x
      apply Susp_ind_beta_merid.
    -
X: Type
P: Susp X -> Type
forall x y : Susp_ind_type,
Susp_ind_inv x $== Susp_ind_inv y -> x $== y intros f g [p q]; cbn in *.
X: Type
P: Susp X -> Type
f, g: Susp_ind_type
p: (f North, f South) = (g North, g South)
q: forall a : X,
transport Susp_ind_data' p
  (fun x : X => apD f (merid x)) a =
apD g (merid a)
forall a : Susp X, f a = g a
      srapply Susp_ind; cbn.
X: Type
P: Susp X -> Type
f, g: Susp_ind_type
p: (f North, f South) = (g North, g South)
q: forall a : X,
transport Susp_ind_data' p
  (fun x : X => apD f (merid x)) a =
apD g (merid a)
f North = g North
X: Type
P: Susp X -> Type
f, g: Susp_ind_type
p: (f North, f South) = (g North, g South)
q: forall a : X,
transport Susp_ind_data' p
  (fun x : X => apD f (merid x)) a =
apD g (merid a)
f South = g South
X: Type
P: Susp X -> Type
f, g: Susp_ind_type
p: (f North, f South) = (g North, g South)
q: forall a : X,
transport Susp_ind_data' p
  (fun x : X => apD f (merid x)) a =
apD g (merid a)
forall x : X,
transport (fun y : Susp X => f y = g y) (merid x)
  ?Goal = ?Goal0
      1: exact (ap fst p).
X: Type
P: Susp X -> Type
f, g: Susp_ind_type
p: (f North, f South) = (g North, g South)
q: forall a : X,
transport Susp_ind_data' p
  (fun x : X => apD f (merid x)) a =
apD g (merid a)
f South = g South
X: Type
P: Susp X -> Type
f, g: Susp_ind_type
p: (f North, f South) = (g North, g South)
q: forall a : X,
transport Susp_ind_data' p
  (fun x : X => apD f (merid x)) a =
apD g (merid a)
forall x : X,
transport (fun y : Susp X => f y = g y) (merid x)
  (ap fst p) = ?Goal
      1: exact (ap snd p).
X: Type
P: Susp X -> Type
f, g: Susp_ind_type
p: (f North, f South) = (g North, g South)
q: forall a : X,
transport Susp_ind_data' p
  (fun x : X => apD f (merid x)) a =
apD g (merid a)
forall x : X,
transport (fun y : Susp X => f y = g y) (merid x)
  (ap fst p) = ap snd p
      intros x; specialize (q x).
X: Type
P: Susp X -> Type
f, g: Susp_ind_type
p: (f North, f South) = (g North, g South)
x: X
q: transport Susp_ind_data' p
  (fun x : X => apD f (merid x)) x =
apD g (merid x)
transport (fun y : Susp X => f y = g y) (merid x)
  (ap fst p) = ap snd p
      apply ds_dp.
X: Type
P: Susp X -> Type
f, g: Susp_ind_type
p: (f North, f South) = (g North, g South)
x: X
q: transport Susp_ind_data' p
  (fun x : X => apD f (merid x)) x =
apD g (merid x)
DPathSquare P (PathSquare.sq_refl_h (merid x))
  (apD f (merid x)) (apD g (merid x)) (ap fst p)
  (ap snd p)
      apply ds_transport_dpath.
X: Type
P: Susp X -> Type
f, g: Susp_ind_type
p: (f North, f South) = (g North, g South)
x: X
q: transport Susp_ind_data' p
  (fun x : X => apD f (merid x)) x =
apD g (merid x)
transport
  (fun y : P North => DPath P (merid x) y (g South))
  (ap fst p)
  (transport
     (fun y : P South => DPath P (merid x) (f North) y)
     (ap snd p) (apD f (merid x))) = apD g (merid x)
      rewrite transport_forall_constant in q.
X: Type
P: Susp X -> Type
f, g: Susp_ind_type
p: (f North, f South) = (g North, g South)
x: X
q: transport
  (fun x0 : P North * P South =>
   DPath P (merid x) (fst x0) (snd x0)) p
  (apD f (merid x)) = apD g (merid x)
transport
  (fun y : P North => DPath P (merid x) y (g South))
  (ap fst p)
  (transport
     (fun y : P South => DPath P (merid x) (f North) y)
     (ap snd p) (apD f (merid x))) = apD g (merid x)
      rewrite <- (eta_path_prod p) in q.
X: Type
P: Susp X -> Type
f, g: Susp_ind_type
p: (f North, f South) = (g North, g South)
x: X
q: transport
  (fun x0 : P North * P South =>
   DPath P (merid x) (fst x0) (snd x0))
  (path_prod (f North, f South) (g North, g South)
     (ap fst p) (ap snd p)) (apD f (merid x)) =
apD g (merid x)
transport
  (fun y : P North => DPath P (merid x) y (g South))
  (ap fst p)
  (transport
     (fun y : P South => DPath P (merid x) (f North) y)
     (ap snd p) (apD f (merid x))) = apD g (merid x)
      rewrite transport_path_prod in q.
X: Type
P: Susp X -> Type
f, g: Susp_ind_type
p: (f North, f South) = (g North, g South)
x: X
q: transport
  (fun x0 : P North =>
   DPath P (merid x)
     (fst (x0, snd (g North, g South)))
     (snd (x0, snd (g North, g South))))
  (ap fst p)
  (transport
     (fun y : P South =>
      DPath P (merid x)
        (fst (fst (f North, f South), y))
        (snd (fst (f North, f South), y)))
     (ap snd p) (apD f (merid x))) =
apD g (merid x)
transport
  (fun y : P North => DPath P (merid x) y (g South))
  (ap fst p)
  (transport
     (fun y : P South => DPath P (merid x) (f North) y)
     (ap snd p) (apD f (merid x))) = apD g (merid x)
      exact q.
  Defined.

End UnivProp.

(** The full non-funext version of the universal property should be formulated with respect to a notion of "wild hom-oo-groupoid", which we don't currently have.  However, we can deduce statements about full higher universal properties that we do have, for instance the statement that a type is local for [functor_susp f] -- expressed in terms of [ooExtendableAlong] -- if and only if all its identity types are local for [f].  (We will use this in [Modalities.Localization] for separated subuniverses.)  To prove this, we again generalize it to the case of dependent types, starting with naturality of the above 0-dimensional universal property. *)

Section UnivPropNat.
  (** We will show that [Susp_ind_inv] for [X] and [Y] commute with precomposition with [f] and [functor_susp f]. *)
  Context {X Y : Type} (f : X -> Y) (P : Susp Y -> Type).

  (** We recall these instances from the previous section. *)
  Local Existing Instances isgraph_Susp_ind_type isgraph_Susp_ind_data'.

  (** Here is an intermediate family of groupoids that we have to use, since precomposition with [f] doesn't land in quite the right place. *)
  Definition Susp_ind_data'' (NS : P North * P South)
    := forall x:X, DPath P (merid (f x)) (fst NS) (snd NS).

  (** This is a 01cat and a 0gpd via global instances. *)
  Local Instance isgraph_Susp_ind_data'' NS : IsGraph (Susp_ind_data'' NS).
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
IsGraph (Susp_ind_data'' NS)
  Proof.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
IsGraph (Susp_ind_data'' NS) apply isgraph_forall; intros; apply isgraph_paths. Defined.

  (** We decompose "precomposition with [f]" into a functor_sigma of two fiberwise functors.  Here is the first. *)
  Definition functor_Susp_ind_data'' (NS : P North * P South)
    : Susp_ind_data' Y P NS -> Susp_ind_data'' NS
    := fun g x => g (f x).

  Local Instance is0functor_functor_Susp_ind_data'' NS
    : Is0Functor (functor_Susp_ind_data'' NS).
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
Is0Functor (functor_Susp_ind_data'' NS)
  Proof.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
Is0Functor (functor_Susp_ind_data'' NS)
    constructor.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
forall a b : Susp_ind_data' Y P NS,
(a $-> b) ->
functor_Susp_ind_data'' NS a $->
functor_Susp_ind_data'' NS b
    intros g h p a.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
g, h: Susp_ind_data' Y P NS
p: g $-> h
a: X
functor_Susp_ind_data'' NS g a $->
functor_Susp_ind_data'' NS h a
    exact (p (f a)).
  Defined.

  (** And here is the second.  This one is actually a fiberwise equivalence of types at each [x]. *)
  Definition equiv_Susp_ind_data' (NS : P North * P South) (x : X)
    : DPath P (merid (f x)) (fst NS) (snd NS)
      <~> DPath (P o functor_susp f) (merid x) (fst NS) (snd NS).
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
x: X
DPath P (merid (f x)) (fst NS) (snd NS) <~>
DPath (P o functor_susp f) (merid x) (fst NS) (snd NS)
  Proof.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
x: X
DPath P (merid (f x)) (fst NS) (snd NS) <~>
DPath (P o functor_susp f) (merid x) (fst NS) (snd NS)
    etransitivity.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
x: X
DPath P (merid (f x)) (fst NS) (snd NS) <~> ?Goal
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
x: X
?Goal <~>
DPath (P o functor_susp f) (merid x) (fst NS) (snd NS)
    -
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
x: X
DPath P (merid (f x)) (fst NS) (snd NS) <~> ?Goal napply (equiv_transport (fun p => DPath P p (fst NS) (snd NS))).
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
x: X
merid (f x) = ?Goal0
      symmetry; apply functor_susp_beta_merid.
    -
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
x: X
DPath P (ap (functor_susp f) (merid x)) (fst NS)
  (snd NS) <~>
DPath (P o functor_susp f) (merid x) (fst NS) (snd NS) symmetry.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
x: X
DPath (P o functor_susp f) (merid x) (fst NS) (snd NS) <~>
DPath P (ap (functor_susp f) (merid x)) (fst NS)
  (snd NS) 
      exact (dp_compose (functor_susp f) P (merid x)).
  Defined.

  Definition functor_Susp_ind_data' (NS : P North * P South)
    : Susp_ind_data'' NS -> Susp_ind_data' X (P o functor_susp f) NS.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
Susp_ind_data'' NS ->
Susp_ind_data' X (P o functor_susp f) NS
  Proof.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
Susp_ind_data'' NS ->
Susp_ind_data' X (P o functor_susp f) NS
    srapply (functor_forall idmap); intros x.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
x: X
(fun a : X => DPath P (merid (f a)) (fst NS) (snd NS))
  (idmap x) ->
(fun b : X =>
 DPath (P o functor_susp f) (merid b) (fst NS)
   (snd NS)) x
    apply equiv_Susp_ind_data'.
  Defined.

  Local Instance is0functor_functor_Susp_ind_data' NS
    : Is0Functor (functor_Susp_ind_data' NS).
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
Is0Functor (functor_Susp_ind_data' NS)
  Proof.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
Is0Functor (functor_Susp_ind_data' NS)
    constructor.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
forall a b : Susp_ind_data'' NS,
(a $-> b) ->
functor_Susp_ind_data' NS a $->
functor_Susp_ind_data' NS b
    intros g h q x.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
g, h: Susp_ind_data'' NS
q: g $-> h
x: X
functor_Susp_ind_data' NS g x $->
functor_Susp_ind_data' NS h x
    cbn; apply ap, ap.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
g, h: Susp_ind_data'' NS
q: g $-> h
x: X
g x = h x
    exact (q x).
  Defined.

  (** And therefore a fiberwise equivalence of 0-groupoids. *)
  Local Instance issurjinj_functor_Susp_ind_data' NS
    : IsSurjInj (functor_Susp_ind_data' NS).
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
IsSurjInj (functor_Susp_ind_data' NS)
  Proof.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
IsSurjInj (functor_Susp_ind_data' NS)
    constructor.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
SplEssSurj (functor_Susp_ind_data' NS)
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
forall x y : Susp_ind_data'' NS,
functor_Susp_ind_data' NS x $==
functor_Susp_ind_data' NS y -> x $== y
    -
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
SplEssSurj (functor_Susp_ind_data' NS) intros g.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
g: Susp_ind_data' X
  (fun x : Susp X => P (functor_susp f x)) NS
{a : Susp_ind_data'' NS &
functor_Susp_ind_data' NS a $== g}
      unshelve econstructor.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
g: Susp_ind_data' X
  (fun x : Susp X => P (functor_susp f x)) NS
Susp_ind_data'' NS
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
g: Susp_ind_data' X
  (fun x : Susp X => P (functor_susp f x)) NS
functor_Susp_ind_data' NS ?a $== g
      +
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
g: Susp_ind_data' X
  (fun x : Susp X => P (functor_susp f x)) NS
Susp_ind_data'' NS intros x.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
g: Susp_ind_data' X
  (fun x : Susp X => P (functor_susp f x)) NS
x: X
DPath P (merid (f x)) (fst NS) (snd NS)
        apply ((equiv_Susp_ind_data' NS x)^-1).
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
g: Susp_ind_data' X
  (fun x : Susp X => P (functor_susp f x)) NS
x: X
DPath (fun x : Susp X => P (functor_susp f x))
  (merid x) (fst NS) (snd NS)
        exact (g x).
      +
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
g: Susp_ind_data' X
  (fun x : Susp X => P (functor_susp f x)) NS
functor_Susp_ind_data' NS
  ((fun x : X => (equiv_Susp_ind_data' NS x)^-1 (g x))
   :
   Susp_ind_data'' NS) $== g intros x.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
g: Susp_ind_data' X
  (fun x : Susp X => P (functor_susp f x)) NS
x: X
functor_Susp_ind_data' NS
  (fun x : X => (equiv_Susp_ind_data' NS x)^-1 (g x))
  x $-> g x
        apply eisretr.
    -
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
forall x y : Susp_ind_data'' NS,
functor_Susp_ind_data' NS x $==
functor_Susp_ind_data' NS y -> x $== y intros g h p x.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
g, h: Susp_ind_data'' NS
p: functor_Susp_ind_data' NS g $==
functor_Susp_ind_data' NS h
x: X
g x $-> h x
      apply (equiv_inj (equiv_Susp_ind_data' NS x)).
X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
g, h: Susp_ind_data'' NS
p: functor_Susp_ind_data' NS g $==
functor_Susp_ind_data' NS h
x: X
equiv_Susp_ind_data' NS x (g x) =
equiv_Susp_ind_data' NS x (h x)
      exact (p x).
  Defined.

  (** Now we put them together. *)
  Definition functor_Susp_ind_data
    : Susp_ind_data Y P -> Susp_ind_data X (P o functor_susp f)
    := fun NSg => (NSg.1 ; (functor_Susp_ind_data' NSg.1 o
                             (functor_Susp_ind_data'' NSg.1)) NSg.2).

  Local Instance is0functor_functor_Susp_ind_data
    : Is0Functor functor_Susp_ind_data.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
Is0Functor functor_Susp_ind_data
  Proof.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
Is0Functor functor_Susp_ind_data
    exact (is0functor_sigma _ _
           (fun NS => functor_Susp_ind_data' NS o functor_Susp_ind_data'' NS)).
  Defined.

  (** Here is the "precomposition with [functor_susp f]" functor. *)
  Definition functor_Susp_ind_type
    : Susp_ind_type Y P -> Susp_ind_type X (P o functor_susp f)
    := fun g => g o functor_susp f.

  Local Instance is0functor_functor_Susp_ind_type
    : Is0Functor functor_Susp_ind_type.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
Is0Functor functor_Susp_ind_type
  Proof.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
Is0Functor functor_Susp_ind_type
    constructor.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
forall a b : Susp_ind_type Y P,
(a $-> b) ->
functor_Susp_ind_type a $-> functor_Susp_ind_type b
    intros g h p a.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
g, h: Susp_ind_type Y P
p: g $-> h
a: Susp X
functor_Susp_ind_type g a $->
functor_Susp_ind_type h a
    exact (p (functor_susp f a)).
  Defined.

  (** And here is the desired naturality square. *)
  Definition Susp_ind_inv_nat
    : (Susp_ind_inv X (P o functor_susp f)) o functor_Susp_ind_type
      $=> functor_Susp_ind_data o (Susp_ind_inv Y P).
X, Y: Type
f: X -> Y
P: Susp Y -> Type
Susp_ind_inv X (P o functor_susp f)
o functor_Susp_ind_type $=>
functor_Susp_ind_data o Susp_ind_inv Y P
  Proof.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
Susp_ind_inv X (P o functor_susp f)
o functor_Susp_ind_type $=>
functor_Susp_ind_data o Susp_ind_inv Y P
    intros g; exists idpath; intros x.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
g: Susp_ind_type Y P
x: X
transport
  (Susp_ind_data' X
     (fun x : Susp X => P (functor_susp f x))) 1
  (Susp_ind_inv X
     (fun x : Susp X => P (functor_susp f x))
     (functor_Susp_ind_type g)).2 x $->
(functor_Susp_ind_data (Susp_ind_inv Y P g)).2 x
    change (apD (fun x0 : Susp X => g (functor_susp f x0)) (merid x) =
            (functor_Susp_ind_data (Susp_ind_inv Y P g)).2 x).
X, Y: Type
f: X -> Y
P: Susp Y -> Type
g: Susp_ind_type Y P
x: X
apD (fun x0 : Susp X => g (functor_susp f x0))
  (merid x) =
(functor_Susp_ind_data (Susp_ind_inv Y P g)).2 x
    refine (dp_apD_compose (functor_susp f) P (merid x) g @ _).
X, Y: Type
f: X -> Y
P: Susp Y -> Type
g: Susp_ind_type Y P
x: X
(dp_compose (functor_susp f) P (merid x))^-1
  (apD g (ap (functor_susp f) (merid x))) =
(functor_Susp_ind_data (Susp_ind_inv Y P g)).2 x
    cbn; apply ap.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
g: Susp_ind_type Y P
x: X
apD g (ap (functor_susp f) (merid x)) =
transport
  (fun p : North = South =>
   transport P p (g North) = g South)
  (functor_susp_beta_merid f x)^ (apD g (merid (f x)))
    apply (moveL_transport_V (fun p => DPath P p (g North) (g South))).
X, Y: Type
f: X -> Y
P: Susp Y -> Type
g: Susp_ind_type Y P
x: X
transport
  (fun p : North = South =>
   DPath P p (g North) (g South))
  (functor_susp_beta_merid f x)
  (apD g (ap (functor_susp f) (merid x))) =
apD g (merid (f x))
    exact (apD (apD g) (functor_susp_beta_merid f x)).
  Defined.

  (** From this we can deduce a equivalence between extendability, which is definitionally equal to split essential surjectivity of a functor between forall 0-groupoids. *)
  Definition extension_iff_functor_susp
    : (forall g, ExtensionAlong (functor_susp f) P g)
      <-> (forall NS g, ExtensionAlong f (fun x => DPath P (merid x) (fst NS) (snd NS)) g).
X, Y: Type
f: X -> Y
P: Susp Y -> Type
(forall g : forall x : Susp X, P (functor_susp f x),
 ExtensionAlong (functor_susp f) P g) <->
(forall (NS : P North * P South)
 (g : forall x : X,
      (fun x0 : Y =>
       DPath P (merid x0) (fst NS) (snd NS)) (f x)),
 ExtensionAlong f
   (fun x : Y => DPath P (merid x) (fst NS) (snd NS))
   g)
  Proof.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
(forall g : forall x : Susp X, P (functor_susp f x),
 ExtensionAlong (functor_susp f) P g) <->
(forall (NS : P North * P South)
 (g : forall x : X,
      (fun x0 : Y =>
       DPath P (merid x0) (fst NS) (snd NS)) (f x)),
 ExtensionAlong f
   (fun x : Y => DPath P (merid x) (fst NS) (snd NS))
   g)
    (** The proof is by chaining logical equivalences. *)
    transitivity (SplEssSurj functor_Susp_ind_type).
X, Y: Type
f: X -> Y
P: Susp Y -> Type
(forall g : forall x : Susp X, P (functor_susp f x),
 ExtensionAlong (functor_susp f) P g) <->
SplEssSurj functor_Susp_ind_type
X, Y: Type
f: X -> Y
P: Susp Y -> Type
SplEssSurj functor_Susp_ind_type <->
(forall (NS : P North * P South)
 (g : forall x : X,
      (fun x0 : Y =>
       DPath P (merid x0) (fst NS) (snd NS)) (f x)),
 ExtensionAlong f
   (fun x : Y => DPath P (merid x) (fst NS) (snd NS))
   g)
    {
X, Y: Type
f: X -> Y
P: Susp Y -> Type
(forall g : forall x : Susp X, P (functor_susp f x),
 ExtensionAlong (functor_susp f) P g) <->
SplEssSurj functor_Susp_ind_type reflexivity. }
X, Y: Type
f: X -> Y
P: Susp Y -> Type
SplEssSurj functor_Susp_ind_type <->
(forall (NS : P North * P South)
 (g : forall x : X,
      (fun x0 : Y =>
       DPath P (merid x0) (fst NS) (snd NS)) (f x)),
 ExtensionAlong f
   (fun x : Y => DPath P (merid x) (fst NS) (snd NS))
   g)
    etransitivity.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
SplEssSurj functor_Susp_ind_type <-> ?Goal
X, Y: Type
f: X -> Y
P: Susp Y -> Type
?Goal <->
(forall (NS : P North * P South)
 (g : forall x : X,
      (fun x0 : Y =>
       DPath P (merid x0) (fst NS) (snd NS)) (f x)),
 ExtensionAlong f
   (fun x : Y => DPath P (merid x) (fst NS) (snd NS))
   g)
    {
X, Y: Type
f: X -> Y
P: Susp Y -> Type
SplEssSurj functor_Susp_ind_type <-> ?Goal refine (isesssurj_iff_commsq Susp_ind_inv_nat); try exact _.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
IsSurjInj (Susp_ind_inv Y P)
X, Y: Type
f: X -> Y
P: Susp Y -> Type
IsSurjInj
  (Susp_ind_inv X
     (fun x : Susp X => P (functor_susp f x)))
      all:apply issurjinj_Susp_ind_inv. }
X, Y: Type
f: X -> Y
P: Susp Y -> Type
SplEssSurj functor_Susp_ind_data <->
(forall (NS : P North * P South)
 (g : forall x : X,
      (fun x0 : Y =>
       DPath P (merid x0) (fst NS) (snd NS)) (f x)),
 ExtensionAlong f
   (fun x : Y => DPath P (merid x) (fst NS) (snd NS))
   g)
    etransitivity.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
SplEssSurj functor_Susp_ind_data <-> ?Goal
X, Y: Type
f: X -> Y
P: Susp Y -> Type
?Goal <->
(forall (NS : P North * P South)
 (g : forall x : X,
      (fun x0 : Y =>
       DPath P (merid x0) (fst NS) (snd NS)) (f x)),
 ExtensionAlong f
   (fun x : Y => DPath P (merid x) (fst NS) (snd NS))
   g)
    {
X, Y: Type
f: X -> Y
P: Susp Y -> Type
SplEssSurj functor_Susp_ind_data <-> ?Goal exact (isesssurj_iff_sigma _ _ 
                (fun NS => functor_Susp_ind_data' NS o functor_Susp_ind_data'' NS)). }
X, Y: Type
f: X -> Y
P: Susp Y -> Type
(forall a : P North * P South,
 SplEssSurj
   ((fun NS : P North * P South =>
     functor_Susp_ind_data' NS
     o functor_Susp_ind_data'' NS) a)) <->
(forall (NS : P North * P South)
 (g : forall x : X,
      (fun x0 : Y =>
       DPath P (merid x0) (fst NS) (snd NS)) (f x)),
 ExtensionAlong f
   (fun x : Y => DPath P (merid x) (fst NS) (snd NS))
   g)
    apply iff_functor_forall; intros [N S]; cbn.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
N: P North
S: P South
SplEssSurj
  (fun x : Susp_ind_data' Y P (N, S) =>
   functor_Susp_ind_data' (N, S)
     (functor_Susp_ind_data'' (N, S) x)) <->
(forall
 g : forall x : X, transport P (merid (f x)) N = S,
 ExtensionAlong f
   (fun x : Y => transport P (merid x) N = S) g)
    etransitivity.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
N: P North
S: P South
SplEssSurj
  (fun x : Susp_ind_data' Y P (N, S) =>
   functor_Susp_ind_data' (N, S)
     (functor_Susp_ind_data'' (N, S) x)) <-> ?Goal
X, Y: Type
f: X -> Y
P: Susp Y -> Type
N: P North
S: P South
?Goal <->
(forall
 g : forall x : X, transport P (merid (f x)) N = S,
 ExtensionAlong f
   (fun x : Y => transport P (merid x) N = S) g)
    {
X, Y: Type
f: X -> Y
P: Susp Y -> Type
N: P North
S: P South
SplEssSurj
  (fun x : Susp_ind_data' Y P (N, S) =>
   functor_Susp_ind_data' (N, S)
     (functor_Susp_ind_data'' (N, S) x)) <-> ?Goal apply iffL_isesssurj; exact _. }
X, Y: Type
f: X -> Y
P: Susp Y -> Type
N: P North
S: P South
SplEssSurj (functor_Susp_ind_data'' (N, S)) <->
(forall
 g : forall x : X, transport P (merid (f x)) N = S,
 ExtensionAlong f
   (fun x : Y => transport P (merid x) N = S) g)
    reflexivity.
  Defined.

  (** We have to close the section now because we have to generalize [extension_iff_functor_susp] over [P]. *)

End UnivPropNat.

(** Now we can iterate, deducing [n]-extendability. *)
Definition extendable_iff_functor_susp
           {X Y : Type} (f : X -> Y) (P : Susp Y -> Type) (n : nat)
  : (ExtendableAlong n (functor_susp f) P)
    <-> (forall NS, ExtendableAlong n f (fun x => DPath P (merid x) (fst NS) (snd NS))).
X, Y: Type
f: X -> Y
P: Susp Y -> Type
n: nat
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
 ExtendableAlong n f
   (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
Proof.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
n: nat
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
 ExtendableAlong n f
   (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
  revert P.
X, Y: Type
f: X -> Y
n: nat
forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
 ExtendableAlong n f
   (fun x : Y => DPath P (merid x) (fst NS) (snd NS))) induction n as [|n IHn]; intros P; [ split; intros; exact tt | ].
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
ExtendableAlong n.+1 (functor_susp f) P <->
(forall NS : P North * P South,
 ExtendableAlong n.+1 f
   (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
  (** It would be nice to be able to do this proof by chaining logical equivalences too, especially since the two parts seem very similar.  But I haven't managed to make that work. *)
  split.
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
ExtendableAlong n.+1 (functor_susp f) P ->
forall NS : P North * P South,
ExtendableAlong n.+1 f
  (fun x : Y => DPath P (merid x) (fst NS) (snd NS))
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
(forall NS : P North * P South,
 ExtendableAlong n.+1 f
   (fun x : Y => DPath P (merid x) (fst NS) (snd NS))) ->
ExtendableAlong n.+1 (functor_susp f) P
  -
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
ExtendableAlong n.+1 (functor_susp f) P ->
forall NS : P North * P South,
ExtendableAlong n.+1 f
  (fun x : Y => DPath P (merid x) (fst NS) (snd NS)) intros [e1 en] [N S]; split.
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
en: forall h k : forall b : Susp Y, P b,
ExtendableAlong n (functor_susp f)
  (fun b : Susp Y => h b = k b)
N: P North
S: P South
forall
g : forall a : X,
    DPath P (merid (f a)) (fst (N, S)) (snd (N, S)),
ExtensionAlong f
  (fun x : Y =>
   DPath P (merid x) (fst (N, S)) (snd (N, S))) g
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
en: forall h k : forall b : Susp Y, P b,
ExtendableAlong n (functor_susp f)
  (fun b : Susp Y => h b = k b)
N: P North
S: P South
forall
h
 k : forall b : Y,
     DPath P (merid b) (fst (N, S)) (snd (N, S)),
ExtendableAlong n f (fun b : Y => h b = k b)
    +
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
en: forall h k : forall b : Susp Y, P b,
ExtendableAlong n (functor_susp f)
  (fun b : Susp Y => h b = k b)
N: P North
S: P South
forall
g : forall a : X,
    DPath P (merid (f a)) (fst (N, S)) (snd (N, S)),
ExtensionAlong f
  (fun x : Y =>
   DPath P (merid x) (fst (N, S)) (snd (N, S))) g apply extension_iff_functor_susp.
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
en: forall h k : forall b : Susp Y, P b,
ExtendableAlong n (functor_susp f)
  (fun b : Susp Y => h b = k b)
N: P North
S: P South
forall g : forall x : Susp X, P (functor_susp f x),
ExtensionAlong (functor_susp f) P g
      exact e1.
    +
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
en: forall h k : forall b : Susp Y, P b,
ExtendableAlong n (functor_susp f)
  (fun b : Susp Y => h b = k b)
N: P North
S: P South
forall
h
 k : forall b : Y,
     DPath P (merid b) (fst (N, S)) (snd (N, S)),
ExtendableAlong n f (fun b : Y => h b = k b) cbn; intros h k.
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
en: forall h k : forall b : Susp Y, P b,
ExtendableAlong n (functor_susp f)
  (fun b : Susp Y => h b = k b)
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
ExtendableAlong n f (fun b : Y => h b = k b)
      pose (h' := Susp_ind P N S h).
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
en: forall h k : forall b : Susp Y, P b,
ExtendableAlong n (functor_susp f)
  (fun b : Susp Y => h b = k b)
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
h':= Susp_ind P N S h: forall y : Susp Y, P y
ExtendableAlong n f (fun b : Y => h b = k b)
      pose (k' := Susp_ind P N S k).
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
en: forall h k : forall b : Susp Y, P b,
ExtendableAlong n (functor_susp f)
  (fun b : Susp Y => h b = k b)
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
h':= Susp_ind P N S h: forall y : Susp Y, P y
k':= Susp_ind P N S k: forall y : Susp Y, P y
ExtendableAlong n f (fun b : Y => h b = k b)
      specialize (en h' k').
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
h':= Susp_ind P N S h: forall y : Susp Y, P y
k':= Susp_ind P N S k: forall y : Susp Y, P y
en: ExtendableAlong n (functor_susp f)
  (fun b : Susp Y => h' b = k' b)
ExtendableAlong n f (fun b : Y => h b = k b)
      assert (IH := fst (IHn _) en (1,1)); clear IHn en.
X, Y: Type
f: X -> Y
n: nat
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
h':= Susp_ind P N S h: forall y : Susp Y, P y
k':= Susp_ind P N S k: forall y : Susp Y, P y
IH: ExtendableAlong n f
  (fun x : Y =>
   DPath (fun b : Susp Y => h' b = k' b)
     (merid x) (fst (1, 1)) (snd (1, 1)))
ExtendableAlong n f (fun b : Y => h b = k b)
      cbn in IH.
X, Y: Type
f: X -> Y
n: nat
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
h':= Susp_ind P N S h: forall y : Susp Y, P y
k':= Susp_ind P N S k: forall y : Susp Y, P y
IH: ExtendableAlong n f
  (fun x : Y =>
   transport (fun b : Susp Y => h' b = k' b)
     (merid x) 1 = 1)
ExtendableAlong n f (fun b : Y => h b = k b)
      refine (extendable_postcompose' n _ _ f _ IH); clear IH.
X, Y: Type
f: X -> Y
n: nat
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
h':= Susp_ind P N S h: forall y : Susp Y, P y
k':= Susp_ind P N S k: forall y : Susp Y, P y
forall b : Y,
transport (fun b0 : Susp Y => h' b0 = k' b0) (merid b)
  1 = 1 <~> h b = k b
      intros y.
X, Y: Type
f: X -> Y
n: nat
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
h':= Susp_ind P N S h: forall y : Susp Y, P y
k':= Susp_ind P N S k: forall y : Susp Y, P y
y: Y
transport (fun b : Susp Y => h' b = k' b) (merid y) 1 =
1 <~> h y = k y
      etransitivity.
X, Y: Type
f: X -> Y
n: nat
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
h':= Susp_ind P N S h: forall y : Susp Y, P y
k':= Susp_ind P N S k: forall y : Susp Y, P y
y: Y
transport (fun b : Susp Y => h' b = k' b) (merid y) 1 =
1 <~> ?Goal0
X, Y: Type
f: X -> Y
n: nat
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
h':= Susp_ind P N S h: forall y : Susp Y, P y
k':= Susp_ind P N S k: forall y : Susp Y, P y
y: Y
?Goal0 <~> h y = k y
      1: napply ds_dp.
X, Y: Type
f: X -> Y
n: nat
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
h':= Susp_ind P N S h: forall y : Susp Y, P y
k':= Susp_ind P N S k: forall y : Susp Y, P y
y: Y
DPathSquare P (PathSquare.sq_refl_h (merid y))
  (apD h' (merid y)) (apD k' (merid y)) 1 1 <~>
h y = k y
      etransitivity.
X, Y: Type
f: X -> Y
n: nat
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
h':= Susp_ind P N S h: forall y : Susp Y, P y
k':= Susp_ind P N S k: forall y : Susp Y, P y
y: Y
DPathSquare P (PathSquare.sq_refl_h (merid y))
  (apD h' (merid y)) (apD k' (merid y)) 1 1 <~> ?Goal0
X, Y: Type
f: X -> Y
n: nat
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
h':= Susp_ind P N S h: forall y : Susp Y, P y
k':= Susp_ind P N S k: forall y : Susp Y, P y
y: Y
?Goal0 <~> h y = k y
      1: apply ds_transport_dpath.
X, Y: Type
f: X -> Y
n: nat
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
h':= Susp_ind P N S h: forall y : Susp Y, P y
k':= Susp_ind P N S k: forall y : Susp Y, P y
y: Y
transport
  (fun y0 : P North => DPath P (merid y) y0 (k' South))
  1
  (transport
     (fun y0 : P South =>
      DPath P (merid y) (h' North) y0) 1
     (apD h' (merid y))) = apD k' (merid y) <~>
h y = k y
      subst h' k'; cbn.
X, Y: Type
f: X -> Y
n: nat
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
y: Y
apD (Susp_ind P N S h) (merid y) =
apD (Susp_ind P N S k) (merid y) <~> h y = k y
      apply equiv_concat_lr.
X, Y: Type
f: X -> Y
n: nat
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
y: Y
h y = apD (Susp_ind P N S h) (merid y)
X, Y: Type
f: X -> Y
n: nat
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
y: Y
apD (Susp_ind P N S k) (merid y) = k y
      *
X, Y: Type
f: X -> Y
n: nat
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
y: Y
h y = apD (Susp_ind P N S h) (merid y) symmetry.
X, Y: Type
f: X -> Y
n: nat
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
y: Y
apD (Susp_ind P N S h) (merid y) = h y exact (Susp_ind_beta_merid P N S h y).
      *
X, Y: Type
f: X -> Y
n: nat
P: Susp Y -> Type
e1: forall
g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
N: P North
S: P South
h, k: forall b : Y, transport P (merid b) N = S
y: Y
apD (Susp_ind P N S k) (merid y) = k y exact (Susp_ind_beta_merid P N S k y).
  -
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
(forall NS : P North * P South,
 ExtendableAlong n.+1 f
   (fun x : Y => DPath P (merid x) (fst NS) (snd NS))) ->
ExtendableAlong n.+1 (functor_susp f) P intros e; split.
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
e: forall NS : P North * P South,
ExtendableAlong n.+1 f
  (fun x : Y =>
   DPath P (merid x) (fst NS) (snd NS))
forall g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
e: forall NS : P North * P South,
ExtendableAlong n.+1 f
  (fun x : Y =>
   DPath P (merid x) (fst NS) (snd NS))
forall h k : forall b : Susp Y, P b,
ExtendableAlong n (functor_susp f)
  (fun b : Susp Y => h b = k b)
    +
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
e: forall NS : P North * P South,
ExtendableAlong n.+1 f
  (fun x : Y =>
   DPath P (merid x) (fst NS) (snd NS))
forall g : forall a : Susp X, P (functor_susp f a),
ExtensionAlong (functor_susp f) P g apply extension_iff_functor_susp.
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
e: forall NS : P North * P South,
ExtendableAlong n.+1 f
  (fun x : Y =>
   DPath P (merid x) (fst NS) (snd NS))
forall (NS : P North * P South)
(g : forall x : X,
     DPath P (merid (f x)) (fst NS) (snd NS)),
ExtensionAlong f
  (fun x : Y => DPath P (merid x) (fst NS) (snd NS)) g
      intros NS; exact (fst (e NS)).
    +
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
e: forall NS : P North * P South,
ExtendableAlong n.+1 f
  (fun x : Y =>
   DPath P (merid x) (fst NS) (snd NS))
forall h k : forall b : Susp Y, P b,
ExtendableAlong n (functor_susp f)
  (fun b : Susp Y => h b = k b) intros h k.
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
e: forall NS : P North * P South,
ExtendableAlong n.+1 f
  (fun x : Y =>
   DPath P (merid x) (fst NS) (snd NS))
h, k: forall b : Susp Y, P b
ExtendableAlong n (functor_susp f)
  (fun b : Susp Y => h b = k b)
      apply (IHn _).
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
e: forall NS : P North * P South,
ExtendableAlong n.+1 f
  (fun x : Y =>
   DPath P (merid x) (fst NS) (snd NS))
h, k: forall b : Susp Y, P b
forall NS : (h North = k North) * (h South = k South),
ExtendableAlong n f
  (fun x : Y =>
   DPath (fun b : Susp Y => h b = k b) (merid x)
     (fst NS) (snd NS))
      intros [p q].
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
e: forall NS : P North * P South,
ExtendableAlong n.+1 f
  (fun x : Y =>
   DPath P (merid x) (fst NS) (snd NS))
h, k: forall b : Susp Y, P b
p: h North = k North
q: h South = k South
ExtendableAlong n f
  (fun x : Y =>
   DPath (fun b : Susp Y => h b = k b) (merid x)
     (fst (p, q)) (snd (p, q)))
      specialize (e (h North, k South)).
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
P: Susp Y -> Type
h, k: forall b : Susp Y, P b
e: ExtendableAlong n.+1 f
  (fun x : Y =>
   DPath P (merid x) (fst (h North, k South))
     (snd (h North, k South)))
p: h North = k North
q: h South = k South
ExtendableAlong n f
  (fun x : Y =>
   DPath (fun b : Susp Y => h b = k b) (merid x)
     (fst (p, q)) (snd (p, q)))
      cbn in *; apply snd in e.
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => transport P (merid x) (fst NS) = snd NS))
P: Susp Y -> Type
h, k: forall b : Susp Y, P b
e: forall
h0
 k0 : forall b : Y,
      transport P (merid b) (h North) = k South,
ExtendableAlong n f (fun b : Y => h0 b = k0 b)
p: h North = k North
q: h South = k South
ExtendableAlong n f
  (fun x : Y =>
   transport (fun b : Susp Y => h b = k b) (merid x) p =
   q)
      refine (extendable_postcompose' n _ _ f _ (e _ _)); intros y.
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => transport P (merid x) (fst NS) = snd NS))
P: Susp Y -> Type
h, k: forall b : Susp Y, P b
e: forall
h0
 k0 : forall b : Y,
      transport P (merid b) (h North) = k South,
ExtendableAlong n f (fun b : Y => h0 b = k0 b)
p: h North = k North
q: h South = k South
y: Y
?Goal y = ?Goal0 y <~>
transport (fun b : Susp Y => h b = k b) (merid y) p =
q
      symmetry.
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => transport P (merid x) (fst NS) = snd NS))
P: Susp Y -> Type
h, k: forall b : Susp Y, P b
e: forall
h0
 k0 : forall b : Y,
      transport P (merid b) (h North) = k South,
ExtendableAlong n f (fun b : Y => h0 b = k0 b)
p: h North = k North
q: h South = k South
y: Y
transport (fun b : Susp Y => h b = k b) (merid y) p =
q <~> ?Goal y = ?Goal0 y
      etransitivity.
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => transport P (merid x) (fst NS) = snd NS))
P: Susp Y -> Type
h, k: forall b : Susp Y, P b
e: forall
h0
 k0 : forall b : Y,
      transport P (merid b) (h North) = k South,
ExtendableAlong n f (fun b : Y => h0 b = k0 b)
p: h North = k North
q: h South = k South
y: Y
transport (fun b : Susp Y => h b = k b) (merid y) p =
q <~> ?Goal1
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => transport P (merid x) (fst NS) = snd NS))
P: Susp Y -> Type
h, k: forall b : Susp Y, P b
e: forall
h0
 k0 : forall b : Y,
      transport P (merid b) (h North) = k South,
ExtendableAlong n f (fun b : Y => h0 b = k0 b)
p: h North = k North
q: h South = k South
y: Y
?Goal1 <~> ?Goal y = ?Goal0 y
      1: napply ds_dp.
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => transport P (merid x) (fst NS) = snd NS))
P: Susp Y -> Type
h, k: forall b : Susp Y, P b
e: forall
h0
 k0 : forall b : Y,
      transport P (merid b) (h North) = k South,
ExtendableAlong n f (fun b : Y => h0 b = k0 b)
p: h North = k North
q: h South = k South
y: Y
DPathSquare P (PathSquare.sq_refl_h (merid y))
  (apD h (merid y)) (apD k (merid y)) p q <~>
?Goal y = ?Goal0 y
      etransitivity.
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => transport P (merid x) (fst NS) = snd NS))
P: Susp Y -> Type
h, k: forall b : Susp Y, P b
e: forall
h0
 k0 : forall b : Y,
      transport P (merid b) (h North) = k South,
ExtendableAlong n f (fun b : Y => h0 b = k0 b)
p: h North = k North
q: h South = k South
y: Y
DPathSquare P (PathSquare.sq_refl_h (merid y))
  (apD h (merid y)) (apD k (merid y)) p q <~> ?Goal1
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => transport P (merid x) (fst NS) = snd NS))
P: Susp Y -> Type
h, k: forall b : Susp Y, P b
e: forall
h0
 k0 : forall b : Y,
      transport P (merid b) (h North) = k South,
ExtendableAlong n f (fun b : Y => h0 b = k0 b)
p: h North = k North
q: h South = k South
y: Y
?Goal1 <~> ?Goal y = ?Goal0 y
      1: apply ds_transport_dpath.
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => transport P (merid x) (fst NS) = snd NS))
P: Susp Y -> Type
h, k: forall b : Susp Y, P b
e: forall
h0
 k0 : forall b : Y,
      transport P (merid b) (h North) = k South,
ExtendableAlong n f (fun b : Y => h0 b = k0 b)
p: h North = k North
q: h South = k South
y: Y
transport
  (fun y0 : P North => DPath P (merid y) y0 (k South))
  p
  (transport
     (fun y0 : P South =>
      DPath P (merid y) (h North) y0) q
     (apD h (merid y))) = apD k (merid y) <~>
?Goal y = ?Goal0 y
      etransitivity.
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => transport P (merid x) (fst NS) = snd NS))
P: Susp Y -> Type
h, k: forall b : Susp Y, P b
e: forall
h0
 k0 : forall b : Y,
      transport P (merid b) (h North) = k South,
ExtendableAlong n f (fun b : Y => h0 b = k0 b)
p: h North = k North
q: h South = k South
y: Y
transport
  (fun y0 : P North => DPath P (merid y) y0 (k South))
  p
  (transport
     (fun y0 : P South =>
      DPath P (merid y) (h North) y0) q
     (apD h (merid y))) = apD k (merid y) <~> ?Goal1
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => transport P (merid x) (fst NS) = snd NS))
P: Susp Y -> Type
h, k: forall b : Susp Y, P b
e: forall
h0
 k0 : forall b : Y,
      transport P (merid b) (h North) = k South,
ExtendableAlong n f (fun b : Y => h0 b = k0 b)
p: h North = k North
q: h South = k South
y: Y
?Goal1 <~> ?Goal y = ?Goal0 y
      1: reflexivity.
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => transport P (merid x) (fst NS) = snd NS))
P: Susp Y -> Type
h, k: forall b : Susp Y, P b
e: forall
h0
 k0 : forall b : Y,
      transport P (merid b) (h North) = k South,
ExtendableAlong n f (fun b : Y => h0 b = k0 b)
p: h North = k North
q: h South = k South
y: Y
transport
  (fun y0 : P North => DPath P (merid y) y0 (k South))
  p
  (transport
     (fun y0 : P South =>
      DPath P (merid y) (h North) y0) q
     (apD h (merid y))) = apD k (merid y) <~>
?Goal y = ?Goal0 y
      symmetry.
X, Y: Type
f: X -> Y
n: nat
IHn: forall P : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P <->
(forall NS : P North * P South,
ExtendableAlong n f (fun x : Y => transport P (merid x) (fst NS) = snd NS))
P: Susp Y -> Type
h, k: forall b : Susp Y, P b
e: forall
h0
 k0 : forall b : Y,
      transport P (merid b) (h North) = k South,
ExtendableAlong n f (fun b : Y => h0 b = k0 b)
p: h North = k North
q: h South = k South
y: Y
?Goal y = ?Goal0 y <~>
transport
  (fun y0 : P North => DPath P (merid y) y0 (k South))
  p
  (transport
     (fun y0 : P South =>
      DPath P (merid y) (h North) y0) q
     (apD h (merid y))) = apD k (merid y)
      apply (equiv_moveR_transport_p (fun y0 : P North => DPath P (merid y) y0 (k South))).
Defined.

(** As usual, deducing oo-extendability is trivial. *)
Definition ooextendable_iff_functor_susp
           {X Y : Type} (f : X -> Y) (P : Susp Y -> Type)
  : (ooExtendableAlong (functor_susp f) P)
    <-> (forall NS, ooExtendableAlong f (fun x => DPath P (merid x) (fst NS) (snd NS))).
X, Y: Type
f: X -> Y
P: Susp Y -> Type
ooExtendableAlong (functor_susp f) P <->
(forall NS : P North * P South,
 ooExtendableAlong f
   (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
Proof.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
ooExtendableAlong (functor_susp f) P <->
(forall NS : P North * P South,
 ooExtendableAlong f
   (fun x : Y => DPath P (merid x) (fst NS) (snd NS)))
  split; intros e.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
e: ooExtendableAlong (functor_susp f) P
forall NS : P North * P South,
ooExtendableAlong f
  (fun x : Y => DPath P (merid x) (fst NS) (snd NS))
X, Y: Type
f: X -> Y
P: Susp Y -> Type
e: forall NS : P North * P South,
ooExtendableAlong f
  (fun x : Y =>
   DPath P (merid x) (fst NS) (snd NS))
ooExtendableAlong (functor_susp f) P
  -
X, Y: Type
f: X -> Y
P: Susp Y -> Type
e: ooExtendableAlong (functor_susp f) P
forall NS : P North * P South,
ooExtendableAlong f
  (fun x : Y => DPath P (merid x) (fst NS) (snd NS)) intros NS n.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
e: ooExtendableAlong (functor_susp f) P
NS: P North * P South
n: nat
ExtendableAlong n f
  (fun x : Y => DPath P (merid x) (fst NS) (snd NS))
    apply extendable_iff_functor_susp.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
e: ooExtendableAlong (functor_susp f) P
NS: P North * P South
n: nat
ExtendableAlong n (functor_susp f) P
    exact (e n).
  -
X, Y: Type
f: X -> Y
P: Susp Y -> Type
e: forall NS : P North * P South,
ooExtendableAlong f
  (fun x : Y =>
   DPath P (merid x) (fst NS) (snd NS))
ooExtendableAlong (functor_susp f) P intros n.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
e: forall NS : P North * P South,
ooExtendableAlong f
  (fun x : Y =>
   DPath P (merid x) (fst NS) (snd NS))
n: nat
ExtendableAlong n (functor_susp f) P
    apply extendable_iff_functor_susp.
X, Y: Type
f: X -> Y
P: Susp Y -> Type
e: forall NS : P North * P South,
ooExtendableAlong f
  (fun x : Y =>
   DPath P (merid x) (fst NS) (snd NS))
n: nat
forall NS : P North * P South,
ExtendableAlong n f
  (fun x : Y => DPath P (merid x) (fst NS) (snd NS))
    intros NS; exact (e NS n).
Defined.

(** ** Nullhomotopies of maps out of suspensions *)

Definition nullhomot_susp_from_paths {X Z : Type} (f : Susp X -> Z)
  (n : NullHomotopy (fun x => ap f (merid x)))
: NullHomotopy f.
X, Z: Type
f: Susp X -> Z
n: NullHomotopy (fun x : X => ap f (merid x))
NullHomotopy f
Proof.
X, Z: Type
f: Susp X -> Z
n: NullHomotopy (fun x : X => ap f (merid x))
NullHomotopy f
  exists (f North).
X, Z: Type
f: Susp X -> Z
n: NullHomotopy (fun x : X => ap f (merid x))
forall x : Susp X, f x = f North
  refine (Susp_ind _ 1 n.1^ _); intros x.
X, Z: Type
f: Susp X -> Z
n: NullHomotopy (fun x : X => ap f (merid x))
x: X
transport (fun y : Susp X => f y = f North) (merid x)
  1 = (n.1)^
  refine (transport_paths_Fl _ _ @ _).
X, Z: Type
f: Susp X -> Z
n: NullHomotopy (fun x : X => ap f (merid x))
x: X
(ap f (merid x))^ @ 1 = (n.1)^
  apply (concat (concat_p1 _)), ap.
X, Z: Type
f: Susp X -> Z
n: NullHomotopy (fun x : X => ap f (merid x))
x: X
ap f (merid x) = n.1 apply n.2.
Defined.

Definition nullhomot_paths_from_susp {X Z : Type} (H_N H_S : Z) (f : X -> H_N = H_S)
  (n : NullHomotopy (Susp_rec H_N H_S f))
: NullHomotopy f.
X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
NullHomotopy f
Proof.
X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
NullHomotopy f
  exists (n.2 North @ (n.2 South)^).
X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
forall x : X, f x = n.2 North @ (n.2 South)^
  intro x.
X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
x: X
f x = n.2 North @ (n.2 South)^ apply moveL_pV.
X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
x: X
f x @ n.2 South = n.2 North
  transitivity (ap (Susp_rec H_N H_S f) (merid x) @ n.2 South).
X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
x: X
f x @ n.2 South =
ap (Susp_rec H_N H_S f) (merid x) @ n.2 South
X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
x: X
ap (Susp_rec H_N H_S f) (merid x) @ n.2 South =
n.2 North
  -
X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
x: X
f x @ n.2 South =
ap (Susp_rec H_N H_S f) (merid x) @ n.2 South apply whiskerR, inverse, Susp_rec_beta_merid.
  -
X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
x: X
ap (Susp_rec H_N H_S f) (merid x) @ n.2 South =
n.2 North lhs napply (concat_Ap n.2 (merid x)).
X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
x: X
n.2 North @ ap (fun _ : Susp X => n.1) (merid x) =
n.2 North
    rhs_V napply concat_p1.
X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
x: X
n.2 North @ ap (fun _ : Susp X => n.1) (merid x) =
n.2 North @ 1
    apply whiskerL, ap_const.
Defined.

(** ** Contractibility of the suspension *)

Instance contr_susp (A : Type) `{Contr A}
  : Contr (Susp A).
A: Type
Contr0: Contr A
Contr (Susp A)
Proof.
A: Type
Contr0: Contr A
Contr (Susp A)
  unfold Susp; exact _.
Defined.

(** ** Connectedness of the suspension *)

Instance isconnected_susp {n : trunc_index} {X : Type}
  `{H : IsConnected n X} : IsConnected n.+1 (Susp X).
n: trunc_index
X: Type
H: IsConnected (Tr n) X
IsConnected (Tr n.+1) (Susp X)
Proof.
n: trunc_index
X: Type
H: IsConnected (Tr n) X
IsConnected (Tr n.+1) (Susp X)
  apply isconnected_from_elim.
n: trunc_index
X: Type
H: IsConnected (Tr n) X
forall C : Type,
In (Tr n.+1) C ->
forall f : Susp X -> C, NullHomotopy f
  intros C H' f.
n: trunc_index
X: Type
H: IsConnected (Tr n) X
C: Type
H': In (Tr n.+1) C
f: Susp X -> C
NullHomotopy f exists (f North).
n: trunc_index
X: Type
H: IsConnected (Tr n) X
C: Type
H': In (Tr n.+1) C
f: Susp X -> C
forall x : Susp X, f x = f North
  assert ({ p0 : f North = f South & forall x:X, ap f (merid x) = p0 })
    as [p0 allpath_p0] by (apply (isconnected_elim n); rapply H').
n: trunc_index
X: Type
H: IsConnected (Tr n) X
C: Type
H': In (Tr n.+1) C
f: Susp X -> C
p0: f North = f South
allpath_p0: forall x : X, ap f (merid x) = p0
forall x : Susp X, f x = f North
  apply (Susp_ind (fun a => f a = f North) 1 p0^).
n: trunc_index
X: Type
H: IsConnected (Tr n) X
C: Type
H': In (Tr n.+1) C
f: Susp X -> C
p0: f North = f South
allpath_p0: forall x : X, ap f (merid x) = p0
forall x : X,
transport (fun a : Susp X => f a = f North) 
  (merid x) 1 = p0^
  intros x.
n: trunc_index
X: Type
H: IsConnected (Tr n) X
C: Type
H': In (Tr n.+1) C
f: Susp X -> C
p0: f North = f South
allpath_p0: forall x : X, ap f (merid x) = p0
x: X
transport (fun a : Susp X => f a = f North) 
  (merid x) 1 = p0^
  apply (concat (transport_paths_Fl _ _)).
n: trunc_index
X: Type
H: IsConnected (Tr n) X
C: Type
H': In (Tr n.+1) C
f: Susp X -> C
p0: f North = f South
allpath_p0: forall x : X, ap f (merid x) = p0
x: X
(ap f (merid x))^ @ 1 = p0^
  apply (concat (concat_p1 _)).
n: trunc_index
X: Type
H: IsConnected (Tr n) X
C: Type
H': In (Tr n.+1) C
f: Susp X -> C
p0: f North = f South
allpath_p0: forall x : X, ap f (merid x) = p0
x: X
(ap f (merid x))^ = p0^
  apply ap, allpath_p0.
Defined.

(** ** Negation map *)

(** The negation map on the suspension is defined by sending [North] to [South] and vice versa, and acting by flipping on the meridians. *)
Definition susp_neg (A : Type) : Susp A -> Susp A
  := Susp_rec South North (fun a => (merid a)^).

(** The negation map is an involution. *)
Definition susp_neg_inv (A : Type) : susp_neg A o susp_neg A == idmap.
A: Type
susp_neg A o susp_neg A == idmap
Proof.
A: Type
susp_neg A o susp_neg A == idmap
  snapply Susp_ind_FFlr.
A: Type
susp_neg A (susp_neg A North) = North
A: Type
susp_neg A (susp_neg A South) = South
A: Type
forall x : A,
ap (susp_neg A) (ap (susp_neg A) (merid x)) @ ?HS =
?HN @ merid x
  1, 2: reflexivity.
A: Type
forall x : A,
ap (susp_neg A) (ap (susp_neg A) (merid x)) @ 1 =
1 @ merid x
  intro a.
A: Type
a: A
ap (susp_neg A) (ap (susp_neg A) (merid a)) @ 1 =
1 @ merid a
  apply equiv_p1_1q.
A: Type
a: A
ap (susp_neg A) (ap (susp_neg A) (merid a)) = merid a
  lhs napply ap.
A: Type
a: A
ap (susp_neg A) (merid a) = ?Goal
A: Type
a: A
ap (susp_neg A) ?Goal = merid a
  1: snapply Susp_rec_beta_merid.
A: Type
a: A
ap (susp_neg A) (merid a)^ = merid a
  lhs napply (ap_V _ (merid a)).
A: Type
a: A
(ap (susp_neg A) (merid a))^ = merid a
  lhs napply ap.
A: Type
a: A
ap (susp_neg A) (merid a) = ?Goal
A: Type
a: A
?Goal^ = merid a
  1: snapply Susp_rec_beta_merid.
A: Type
a: A
((merid a)^)^ = merid a
  napply inv_V.
Defined.

Instance isequiv_susp_neg (A : Type) : IsEquiv (susp_neg A)
  := isequiv_involution (susp_neg A) (susp_neg_inv A).

Definition equiv_susp_neg (A : Type) : Susp A <~> Susp A
  := Build_Equiv _ _ (susp_neg A) _.

(** By using the suspension functor, we can also define another negation map on [Susp (Susp A))]. It turns out these are homotopic. *)
Definition susp_neg_stable (A : Type)
  : functor_susp (susp_neg A) == susp_neg (Susp A).
A: Type
functor_susp (susp_neg A) == susp_neg (Susp A)
Proof.
A: Type
functor_susp (susp_neg A) == susp_neg (Susp A)
  snapply Susp_ind_FlFr; simpl.
A: Type
North = South
A: Type
South = North
A: Type
forall x : Susp A,
ap (functor_susp (susp_neg A)) (merid x) @ ?Goal0 =
?Goal @ ap (susp_neg (Susp A)) (merid x)
  -
A: Type
North = South exact (merid North).
  -
A: Type
South = North exact (merid South)^.
  -
A: Type
forall x : Susp A,
ap (functor_susp (susp_neg A)) (merid x) @
(merid South)^ =
merid North @ ap (susp_neg (Susp A)) (merid x) intro x.
A: Type
x: Susp A
ap (functor_susp (susp_neg A)) (merid x) @
(merid South)^ =
merid North @ ap (susp_neg (Susp A)) (merid x)
    lhs napply whiskerR.
A: Type
x: Susp A
ap (functor_susp (susp_neg A)) (merid x) = ?Goal
A: Type
x: Susp A
?Goal @ (merid South)^ =
merid North @ ap (susp_neg (Susp A)) (merid x)
    1: napply functor_susp_beta_merid.
A: Type
x: Susp A
merid (susp_neg A x) @ (merid South)^ =
merid North @ ap (susp_neg (Susp A)) (merid x)
    rhs napply whiskerL.
A: Type
x: Susp A
merid (susp_neg A x) @ (merid South)^ =
merid North @ ?Goal
A: Type
x: Susp A
ap (susp_neg (Susp A)) (merid x) = ?Goal
    2: napply Susp_rec_beta_merid.
A: Type
x: Susp A
merid (susp_neg A x) @ (merid South)^ =
merid North @ (merid x)^
    revert x; snapply Susp_ind_FlFr; simpl.
A: Type
merid South @ (merid South)^ =
merid North @ (merid North)^
A: Type
merid North @ (merid South)^ =
merid North @ (merid South)^
A: Type
forall x : A,
ap
  (fun x0 : Susp A =>
   merid (susp_neg A x0) @ (merid South)^) (merid x) @
?Goal0 =
?Goal @
ap (fun x0 : Susp A => merid North @ (merid x0)^)
  (merid x)
    +
A: Type
merid South @ (merid South)^ =
merid North @ (merid North)^ exact (concat_pV _ @ (concat_pV _)^).
    +
A: Type
merid North @ (merid South)^ =
merid North @ (merid South)^ reflexivity.
    +
A: Type
forall x : A,
ap
  (fun x0 : Susp A =>
   merid (susp_neg A x0) @ (merid South)^) (merid x) @
1 =
(concat_pV (merid South) @ (concat_pV (merid North))^) @
ap (fun x0 : Susp A => merid North @ (merid x0)^)
  (merid x) intro a.
A: Type
a: A
ap
  (fun x : Susp A =>
   merid (susp_neg A x) @ (merid South)^) (merid a) @
1 =
(concat_pV (merid South) @ (concat_pV (merid North))^) @
ap (fun x : Susp A => merid North @ (merid x)^)
  (merid a)
      lhs napply concat_p1.
A: Type
a: A
ap
  (fun x : Susp A =>
   merid (susp_neg A x) @ (merid South)^) (merid a) =
(concat_pV (merid South) @ (concat_pV (merid North))^) @
ap (fun x : Susp A => merid North @ (merid x)^)
  (merid a)
      lhs napply (ap_compose _ (fun y => merid y @ _) (merid a)).
A: Type
a: A
ap (fun y : Susp A => merid y @ (merid South)^)
  (ap (susp_neg A) (merid a)) =
(concat_pV (merid South) @ (concat_pV (merid North))^) @
ap (fun x : Susp A => merid North @ (merid x)^)
  (merid a)
      lhs napply ap.
A: Type
a: A
ap (susp_neg A) (merid a) = ?Goal
A: Type
a: A
ap (fun y : Susp A => merid y @ (merid South)^) ?Goal =
(concat_pV (merid South) @ (concat_pV (merid North))^) @
ap (fun x : Susp A => merid North @ (merid x)^)
  (merid a)
      1: napply Susp_rec_beta_merid.
A: Type
a: A
ap (fun y : Susp A => merid y @ (merid South)^)
  (merid a)^ =
(concat_pV (merid South) @ (concat_pV (merid North))^) @
ap (fun x : Susp A => merid North @ (merid x)^)
  (merid a)
      simpl.
A: Type
a: A
ap (fun y : Susp A => merid y @ (merid South)^)
  (merid a)^ =
(concat_pV (merid South) @ (concat_pV (merid North))^) @
ap (fun x : Susp A => merid North @ (merid x)^)
  (merid a)
      generalize (merid a) as p.
A: Type
a: A
forall p : North = South,
ap (fun y : Susp A => merid y @ (merid South)^) p^ =
(concat_pV (merid South) @ (concat_pV (merid North))^) @
ap (fun x : Susp A => merid North @ (merid x)^) p
      generalize (@South A) as s.
A: Type
a: A
forall (s : Susp A) (p : North = s),
ap (fun y : Susp A => merid y @ (merid s)^) p^ =
(concat_pV (merid s) @ (concat_pV (merid North))^) @
ap (fun x : Susp A => merid North @ (merid x)^) p
      intros s p; destruct p.
A: Type
a: A
ap (fun y : Susp A => merid y @ (merid North)^) 1^ =
(concat_pV (merid North) @ (concat_pV (merid North))^) @
ap (fun x : Susp A => merid North @ (merid x)^) 1
      simpl.
A: Type
a: A
1 =
(concat_pV (merid North) @ (concat_pV (merid North))^) @
1
      symmetry.
A: Type
a: A
(concat_pV (merid North) @ (concat_pV (merid North))^) @
1 = 1
      lhs napply concat_p1.
A: Type
a: A
concat_pV (merid North) @ (concat_pV (merid North))^ =
1
      apply concat_pV.
Defined.

(** [susp_neg] is a natural equivalence on the suspension functor. *)
Definition susp_neg_natural {A B : Type} (f : A -> B)
  : susp_neg B o functor_susp f == functor_susp f o susp_neg A.
A, B: Type
f: A -> B
susp_neg B o functor_susp f ==
functor_susp f o susp_neg A
Proof.
A, B: Type
f: A -> B
susp_neg B o functor_susp f ==
functor_susp f o susp_neg A
  snapply Susp_ind_FFlFFr.
A, B: Type
f: A -> B
susp_neg B (functor_susp f North) =
functor_susp f (susp_neg A North)
A, B: Type
f: A -> B
susp_neg B (functor_susp f South) =
functor_susp f (susp_neg A South)
A, B: Type
f: A -> B
forall x : A,
ap (susp_neg B) (ap (functor_susp f) (merid x)) @ ?HS =
?HN @ ap (functor_susp f) (ap (susp_neg A) (merid x))
  1, 2: reflexivity.
A, B: Type
f: A -> B
forall x : A,
ap (susp_neg B) (ap (functor_susp f) (merid x)) @ 1 =
1 @ ap (functor_susp f) (ap (susp_neg A) (merid x))
  intro a.
A, B: Type
f: A -> B
a: A
ap (susp_neg B) (ap (functor_susp f) (merid a)) @ 1 =
1 @ ap (functor_susp f) (ap (susp_neg A) (merid a))
  apply equiv_p1_1q.
A, B: Type
f: A -> B
a: A
ap (susp_neg B) (ap (functor_susp f) (merid a)) =
ap (functor_susp f) (ap (susp_neg A) (merid a))
  lhs napply (ap _ (Susp_rec_beta_merid _)).
A, B: Type
f: A -> B
a: A
ap (susp_neg B) (merid (f a)) =
ap (functor_susp f) (ap (susp_neg A) (merid a))
  rhs napply (ap _ (Susp_rec_beta_merid _)).
A, B: Type
f: A -> B
a: A
ap (susp_neg B) (merid (f a)) =
ap (functor_susp f) (merid a)^
  rhs napply (ap_V _ (merid a)).
A, B: Type
f: A -> B
a: A
ap (susp_neg B) (merid (f a)) =
(ap (functor_susp f) (merid a))^
  rhs napply (ap _ (Susp_rec_beta_merid _)).
A, B: Type
f: A -> B
a: A
ap (susp_neg B) (merid (f a)) = (merid (f a))^
  napply Susp_rec_beta_merid.
Defined.