HoTT.Homotopy.Suspension.v.alectryon.json

From HoTT Require Import Basics.From HoTT Require Import Basics.
Require Import Types.
Require Import Cubical.DPath Cubical.DPathSquare.
From HoTT.WildCat Require Import Core Forall Universe Paths Sigma
  EquivGpd NatTrans.
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 x0 : X, transport P (merid x0) 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 x0 : X, transport P (merid x0) 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 x0 : X, ap f (merid x0) @ HS = HN @ ap g (merid x0)
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 x0 : X, ap f (merid x0) @ HS = HN @ ap g (merid x0)
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 x0 : X, ap g (ap f (merid x0)) @ HS = HN @ merid x0
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 x0 : X, ap g (ap f (merid x0)) @ HS = HN @ merid x0
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 x0 : X, ap g (ap f (merid x0)) @ HS = HN @ ap h (merid x0)
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 x0 : X, ap g (ap f (merid x0)) @ HS = HN @ ap h (merid x0)
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 x0 : X, ap g (ap f (merid x0)) @ HS = HN @ ap g' (ap f' (merid x0))
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 x0 : X, ap g (ap f (merid x0)) @ HS = HN @ ap g' (ap f' (merid x0))
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 x0 : X, f x0 @ q = p @ f' x0
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 x0 : X, f x0 @ q = p @ f' x0
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 x0 : X, f x0 @ q = p @ f' x0
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 x0 : X => apD f (merid x0)) 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 x0 : X => apD f (merid x0)))
  (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 x0 : X => apD f (merid x0)))
   (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 x0 : X => apD f (merid x0)))
   (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 x0 : X => apD f (merid x0)))
  (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 x0 : X => ap f (merid x0))) (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 x0 : X => ap f (merid x0))) (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 x0 : Susp X => functor_susp g (functor_susp f x0)) (merid x)
  apply equiv_p1_1q.X, Y, Z: Type
f: X -> Y
g: Y -> Z
x: X
ap (functor_susp (fun x0 : X => g (f x0))) (merid x) =
ap (fun x0 : Susp X => functor_susp g (functor_susp f x0)) (merid x)
  lhs napply functor_susp_beta_merid; symmetry.X, Y, Z: Type
f: X -> Y
g: Y -> Z
x: X
ap (fun x0 : Susp X => functor_susp g (functor_susp f x0)) (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
{p0 : (f North, f South) = (g North, g South) &
forall a : X,
transport Susp_ind_data' p0 (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 x0 : X => apD f (merid x0)) 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 x0 : X => apD f (merid x0)) 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 x0 : X => apD f (merid x0)) 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 x0 : X => apD f (merid x0)) 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 x0 : Susp X => P (functor_susp f x0)) 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 x0 : Susp X => P (functor_susp f x0)) NS
x: X
DPath (fun x0 : Susp X => P (functor_susp f x0)) (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 x0 : Susp X => P (functor_susp f x0)) NS
x: X
functor_Susp_ind_data' NS
  (fun x0 : X => (equiv_Susp_ind_data' NS x0)^-1 (g x0)) 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_functor_sigma_id _ _
           (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 x0 : Susp X => P (functor_susp f x0))) 1
  (Susp_ind_inv X (fun x0 : Susp X => P (functor_susp f x0))
     (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 h0 k0 : forall b : Susp Y, P b,
ExtendableAlong n (functor_susp f) (fun b : Susp Y => h0 b = k0 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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 h0 k0 : forall b : Susp Y, P b,
ExtendableAlong n (functor_susp f) (fun b : Susp Y => h0 b = k0 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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 h0 k0 : forall b : Susp Y, P b,
ExtendableAlong n (functor_susp f) (fun b : Susp Y => h0 b = k0 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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 y0 : Susp Y, P y0
k':= Susp_ind P N S k: forall y0 : Susp Y, P y0
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 y0 : Susp Y, P y0
k':= Susp_ind P N S k: forall y0 : Susp Y, P y0
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 y0 : Susp Y, P y0
k':= Susp_ind P N S k: forall y0 : Susp Y, P y0
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 y0 : Susp Y, P y0
k':= Susp_ind P N S k: forall y0 : Susp Y, P y0
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 y0 : Susp Y, P y0
k':= Susp_ind P N S k: forall y0 : Susp Y, P y0
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 y0 : Susp Y, P y0
k':= Susp_ind P N S k: forall y0 : Susp Y, P y0
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 y0 : Susp Y, P y0
k':= Susp_ind P N S k: forall y0 : Susp Y, P y0
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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => DPath P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => transport P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => transport P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => transport P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => transport P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => transport P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => transport P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => transport P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => transport P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => transport P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => transport P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => transport P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => transport P0 (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 P0 : Susp Y -> Type,
ExtendableAlong n (functor_susp f) P0 <->
(forall NS : P0 North * P0 South,
 ExtendableAlong n f (fun x : Y => transport P0 (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 x0 : X => ap f (merid x0))
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 x0 : X => ap f (merid x0))
x: X
(ap f (merid x))^ @ 1 = (n.1)^
  apply (concat (concat_p1 _)), ap.X, Z: Type
f: Susp X -> Z
n: NullHomotopy (fun x0 : X => ap f (merid x0))
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 x0 : X, ap f (merid x0) = 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 x0 : X, ap f (merid x0) = 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 x0 : X, ap f (merid x0) = 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.