Suspension.v

(* -*- mode: coq; mode: visual-line -*- *)
Require Import Basics.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.
Require Import Cubical.
Require Import WildCat.
Require Import Colimits.Pushout.
Require Import NullHomotopy.
Require Import Truncations.Core.
Require Import Modalities.Modality.
Require Import Extensions.

(** * The suspension of a type *)

Generalizable Variables X A B f g n.

Local Open Scope path_scope.

(* ** Definition of suspension *)

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

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

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

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

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

(** A version of [Susp_ind] specifically for proving that two functions defined on a suspension are homotopic. *)
Definition Susp_ind_FlFr {X Y : Type} (f g : Susp X -> Y)
  (HN : f North = g North)
  (HS : f South = g South)
  (Hmerid : forall x, ap f (merid x) @ HS = HN @ ap g (merid x))
  : f == g.X, Y: Type
f, g: Susp X -> Y
HN: f North = g North
HS: f South = g South
Hmerid: forall x : X,
ap f (merid x) @ HS = HN @ ap g (merid x)
f == g
Proof.X, Y: Type
f, g: Susp X -> Y
HN: f North = g North
HS: f South = g South
Hmerid: forall x : X,
ap f (merid x) @ HS = HN @ ap g (merid x)
f == g
  snrapply Susp_ind.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)
(fun y : Susp X => f y = g y) North
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)
(fun y : Susp X => f y = g y) South
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) ?H_N =
?H_S
  -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)
(fun y : Susp X => f y = g y) North exact HN.
  -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)
(fun y : Susp X => f y = g y) South exact 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 intro x.X, Y: Type
f, g: Susp X -> Y
HN: f North = g North
HS: f South = g South
Hmerid: forall x : X,
ap f (merid x) @ HS = HN @ ap g (merid x)
x: X
transport (fun y : Susp X => f y = g y) (merid x) HN =
HS
    nrapply transport_paths_FlFr'.X, Y: Type
f, g: Susp X -> Y
HN: f North = g North
HS: f South = g South
Hmerid: forall x : X,
ap f (merid x) @ HS = HN @ ap g (merid x)
x: X
ap f (merid x) @ HS = HN @ ap g (merid x)
    apply Hmerid.
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.

(** ** 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_eta_homot {X : Type} {P : Susp X -> Type} (f : forall y, P y)
  : f == Susp_ind P (f North) (f South) (fun x => apD f (merid x)).X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
f ==
Susp_ind P (f North) (f South)
  (fun x : X => apD f (merid x))
Proof.X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
f ==
Susp_ind P (f North) (f South)
  (fun x : X => apD f (merid x))
  unfold pointwise_paths.X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
forall x : Susp X,
f x =
Susp_ind P (f North) (f South)
  (fun x0 : X => apD f (merid x0)) x refine (Susp_ind _ 1 1 _).X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
forall x : X,
transport
  (fun y : Susp X =>
   f y =
   Susp_ind P (f North) (f South)
     (fun x0 : X => apD f (merid x0)) y) (merid x) 1 =
1
  intros x.X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
x: X
transport
  (fun y : Susp X =>
   f y =
   Susp_ind P (f North) (f South)
     (fun x : X => apD f (merid x)) y) (merid x) 1 = 1
  refine (transport_paths_FlFr_D
    (g := Susp_ind P (f North) (f South) (fun x : X => apD f (merid x)))
    _ _ @ _); simpl.X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
x: X
((apD f (merid x))^ @ 1) @
apD
  (Susp_ind P (f North) (f South)
     (fun x : X => apD f (merid x))) (merid x) = 1
  apply moveR_pM.X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
x: X
(apD f (merid x))^ @ 1 =
1 @
(apD
   (Susp_ind P (f North) (f South)
      (fun x : X => apD f (merid x))) (merid x))^
  apply equiv_p1_1q.X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
x: X
(apD f (merid x))^ =
(apD
   (Susp_ind P (f North) (f South)
      (fun x : X => apD f (merid x))) (merid x))^
  apply ap, inverse.X: Type
P: Susp X -> Type
f: forall y : Susp X, P y
x: X
apD
  (Susp_ind P (f North) (f South)
     (fun x : X => apD f (merid x))) (merid x) =
apD f (merid x) refine (Susp_ind_beta_merid _ _ _ _ _).
Defined.

Definition Susp_rec_eta_homot {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))
  snrapply Susp_ind_FlFr.X, Y: Type
f: Susp X -> Y
f North =
Susp_rec (f North) (f South)
  (fun x : X => ap f (merid x)) North
X, Y: Type
f: Susp X -> Y
f South =
Susp_rec (f North) (f South)
  (fun x : X => ap f (merid x)) South
X, Y: Type
f: Susp X -> Y
forall x : X,
ap f (merid x) @ ?HS =
?HN @
ap
  (Susp_rec (f North) (f South)
     (fun x0 : X => ap f (merid x0))) (merid x)
  1, 2: reflexivity.X, Y: Type
f: Susp X -> Y
forall x : X,
ap f (merid x) @ 1 =
1 @
ap
  (Susp_rec (f North) (f South)
     (fun x0 : X => ap f (merid x0))) (merid x)
  intro x.X, Y: Type
f: Susp X -> Y
x: X
ap f (merid x) @ 1 =
1 @
ap
  (Susp_rec (f North) (f South)
     (fun x : X => ap f (merid x))) (merid x)
  apply equiv_p1_1q.X, Y: Type
f: Susp X -> Y
x: X
ap f (merid x) =
ap
  (Susp_rec (f North) (f South)
     (fun x : X => ap f (merid x))) (merid x)
  exact (Susp_rec_beta_merid _)^.
Defined.

Definition Susp_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_eta_homot 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_homot 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
  snrapply Susp_ind_FlFr.X, Y, Z: Type
f: X -> Y
g: Y -> Z
functor_susp (g o f) North =
(fun x : Susp X => functor_susp g (functor_susp f x))
  North
X, Y, Z: Type
f: X -> Y
g: Y -> Z
functor_susp (g o f) South =
(fun x : Susp X => functor_susp g (functor_susp f x))
  South
X, Y, Z: Type
f: X -> Y
g: Y -> Z
forall x : X,
ap (functor_susp (g o f)) (merid x) @ ?HS =
?HN @
ap
  (fun x0 : Susp X =>
   functor_susp g (functor_susp f x0)) (merid x)
  1,2: reflexivity.X, Y, Z: Type
f: X -> Y
g: Y -> Z
forall x : X,
ap (functor_susp (g o f)) (merid x) @ 1 =
1 @
ap
  (fun x0 : Susp X =>
   functor_susp g (functor_susp f x0)) (merid x)
  intro x.X, Y, Z: Type
f: X -> Y
g: Y -> Z
x: X
ap (functor_susp (g o f)) (merid x) @ 1 =
1 @
ap
  (fun x : Susp X => functor_susp g (functor_susp f x))
  (merid x)
  apply equiv_p1_1q.X, Y, Z: Type
f: X -> Y
g: Y -> Z
x: X
ap (functor_susp (fun x : X => g (f x))) (merid x) =
ap
  (fun x : Susp X => functor_susp g (functor_susp f x))
  (merid x)
  lhs nrapply functor_susp_beta_merid; symmetry.X, Y, Z: Type
f: X -> Y
g: Y -> Z
x: X
ap
  (fun x : Susp X => functor_susp g (functor_susp f x))
  (merid x) = merid (g (f x))
  lhs nrefine (ap_compose (functor_susp f) _ (merid x)).X, Y, Z: Type
f: X -> Y
g: Y -> Z
x: X
ap (functor_susp g) (ap (functor_susp f) (merid x)) =
merid (g (f x))
  lhs nrefine (ap _ (functor_susp_beta_merid _ _)).X, Y, Z: Type
f: X -> Y
g: Y -> Z
x: X
ap (functor_susp g) (merid (f x)) = merid (g (f x))
  apply functor_susp_beta_merid.
Defined.

Definition functor_susp_idmap {X}
  : functor_susp idmap == (idmap : Susp X -> Susp X).X: Type
functor_susp idmap == (idmap : Susp X -> Susp X)
Proof.X: Type
functor_susp idmap == (idmap : Susp X -> Susp X)
  snrapply 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 nrapply 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 nrapply (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 nrapply (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.

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

Global 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}
  snrapply 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.

  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.

  Local Instance is01cat_Susp_ind_type : Is01Cat Susp_ind_type.X: Type
P: Susp X -> Type
Is01Cat Susp_ind_type
  Proof.X: Type
P: Susp X -> Type
Is01Cat Susp_ind_type apply is01cat_forall; intros; apply is01cat_paths. Defined.

  Local Instance is0gpd_Susp_ind_type : Is0Gpd Susp_ind_type.X: Type
P: Susp X -> Type
Is0Gpd Susp_ind_type
  Proof.X: Type
P: Susp X -> Type
Is0Gpd Susp_ind_type apply is0gpd_forall; intros; apply is0gpd_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).

  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.

  Local Instance is01cat_Susp_ind_data' NS : Is01Cat (Susp_ind_data' NS).X: Type
P: Susp X -> Type
NS: P North * P South
Is01Cat (Susp_ind_data' NS)
  Proof.X: Type
P: Susp X -> Type
NS: P North * P South
Is01Cat (Susp_ind_data' NS) apply is01cat_forall; intros; apply is01cat_paths. Defined.

  Local Instance is0gpd_Susp_ind_data' NS : Is0Gpd (Susp_ind_data' NS).X: Type
P: Susp X -> Type
NS: P North * P South
Is0Gpd (Susp_ind_data' NS)
  Proof.X: Type
P: Susp X -> Type
NS: P North * P South
Is0Gpd (Susp_ind_data' NS) apply is0gpd_forall; intros; apply is0gpd_paths. Defined.

  (** Here is the codomain itself. *)
  Definition Susp_ind_data := sig Susp_ind_data'.

  Local Instance is01cat_Susp_ind_data : Is01Cat Susp_ind_data.X: Type
P: Susp X -> Type
Is01Cat Susp_ind_data
  Proof.X: Type
P: Susp X -> Type
Is01Cat Susp_ind_data rapply is01cat_sigma. Defined.

  Local Instance is0gpd_Susp_ind_data : Is0Gpd Susp_ind_data.X: Type
P: Susp X -> Type
Is0Gpd Susp_ind_data
  Proof.X: Type
P: Susp X -> Type
Is0Gpd Susp_ind_data rapply is0gpd_sigma. Defined.

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

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

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

End UnivProp.

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

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

  (** We recall all those instances from the previous section. *)
  Local Existing Instances isgraph_Susp_ind_type is01cat_Susp_ind_type is0gpd_Susp_ind_type isgraph_Susp_ind_data' is01cat_Susp_ind_data' is0gpd_Susp_ind_data' is01cat_Susp_ind_data is0gpd_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).

  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.

  Local Instance is01cat_Susp_ind_data'' NS : Is01Cat (Susp_ind_data'' NS).X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
Is01Cat (Susp_ind_data'' NS)
  Proof.X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
Is01Cat (Susp_ind_data'' NS) apply is01cat_forall; intros; apply is01cat_paths. Defined.

  Local Instance is0gpd_Susp_ind_data'' NS : Is0Gpd (Susp_ind_data'' NS).X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
Is0Gpd (Susp_ind_data'' NS)
  Proof.X, Y: Type
f: X -> Y
P: Susp Y -> Type
NS: P North * P South
Is0Gpd (Susp_ind_data'' NS) apply is0gpd_forall; intros; apply is0gpd_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 nrapply (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) 
      apply (dp_compose (functor_susp f) P (merid x)).
  Defined.

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

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

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

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

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

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

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

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

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

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

End UnivPropNat.

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

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

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

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

Definition nullhomot_paths_from_susp {X Z : Type} (H_N H_S : Z) (f : X -> H_N = H_S)
  (n : NullHomotopy (Susp_rec H_N H_S f))
: NullHomotopy f.X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
NullHomotopy f
Proof.X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
NullHomotopy f
  exists (n.2 North @ (n.2 South)^).X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
forall x : X, f x = n.2 North @ (n.2 South)^
  intro x.X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
x: X
f x = n.2 North @ (n.2 South)^ apply moveL_pV.X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
x: X
f x @ n.2 South = n.2 North
  transitivity (ap (Susp_rec H_N H_S f) (merid x) @ n.2 South).X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
x: X
f x @ n.2 South =
ap (Susp_rec H_N H_S f) (merid x) @ n.2 South
X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
x: X
ap (Susp_rec H_N H_S f) (merid x) @ n.2 South =
n.2 North
  -X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
x: X
f x @ n.2 South =
ap (Susp_rec H_N H_S f) (merid x) @ n.2 South apply whiskerR, inverse, Susp_rec_beta_merid.
  -X, Z: Type
H_N, H_S: Z
f: X -> H_N = H_S
n: NullHomotopy (Susp_rec H_N H_S f)
x: X
ap (Susp_rec H_N H_S f) (merid x) @ n.2 South =
n.2 North refine (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
    apply (concatR (concat_p1 _)), whiskerL.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 (fun _ : Susp X => n.1) (merid x) = 1 apply ap_const.
Defined.

(** ** Contractibility of the suspension *)

Global 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 *)

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