(* -*- mode: coq; mode: visual-line -*- *)

(** * The flattening lemma. *)

Require Import HoTT.Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Paths Types.Forall Types.Sigma Types.Arrow Types.Universe.
Local Open Scope path_scope.
Require Import HoTT.Colimits.Coeq.

(** The base HIT [W] is just a homotopy coequalizer [Coeq]. *)

(** TODO: Make the names in this file more usable, move it into [Coeq.v], and use it to derive corresponding flattening lemmas for [pushout], etc. *)

(** Now we define the flattened HIT which will be equivalent to the total space of a fibration over [W]. *)

Module Export FlattenedHIT.

Private Inductive Wtil (A B : Type) (f g : B -> A)
  (C : A -> Type) (D : forall b, C (f b) <~> C (g b))
  : Type :=
| cct : forall a, C a -> Wtil A B f g C D.

Arguments cct {A B f g C D} a c.

Axiom ppt : forall {A B f g C D} (b:B) (y:C (f b)),
  @cct A B f g C D (f b) y = cct (g b) (D b y).

Definition Wtil_ind {A B f g C D} (Q : Wtil A B f g C D -> Type)
  (cct' : forall a x, Q (cct a x))
  (ppt' : forall b y, (ppt b y) # (cct' (f b) y) = cct' (g b) (D b y))
  : forall w, Q w
  := fun w => match w with cct a x => fun _ => cct' a x end ppt'.

Axiom Wtil_ind_beta_ppt
  : forall {A B f g C D} (Q : Wtil A B f g C D -> Type)
    (cct' : forall a x, Q (cct a x))
    (ppt' : forall b y, (ppt b y) # (cct' (f b) y) = cct' (g b) (D b y))
    (b:B) (y : C (f b)),
    apD (Wtil_ind Q cct' ppt') (ppt b y) = ppt' b y.

End FlattenedHIT.

Definition Wtil_rec {A B f g C} {D : forall b, C (f b) <~> C (g b)}
  (Q : Type) (cct' : forall a (x : C a), Q)
  (ppt' : forall b (y : C (f b)), cct' (f b) y = cct' (g b) (D b y))
  : Wtil A B f g C D -> Q
  := Wtil_ind (fun _ => Q) cct' (fun b y => transport_const _ _ @ ppt' b y).

Definition Wtil_rec_beta_ppt
  {A B f g C} {D : forall b, C (f b) <~> C (g b)}
  (Q : Type) (cct' : forall a (x : C a), Q)
  (ppt' : forall (b:B) (y : C (f b)), cct' (f b) y = cct' (g b) (D b y))
  (b:B) (y: C (f b))
  : ap (@Wtil_rec A B f g C D Q cct' ppt') (ppt b y) = ppt' b y.
A, B: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
Q: Type
cct': forall a : A, C a -> Q
ppt': forall (b : B) (y : C (f b)),
cct' (f b) y = cct' (g b) (D b y)
b: B
y: C (f b)
ap (Wtil_rec Q cct' ppt') (ppt b y) = ppt' b y
Proof.
A, B: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
Q: Type
cct': forall a : A, C a -> Q
ppt': forall (b : B) (y : C (f b)),
cct' (f b) y = cct' (g b) (D b y)
b: B
y: C (f b)
ap (Wtil_rec Q cct' ppt') (ppt b y) = ppt' b y
  unfold Wtil_rec.
A, B: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
Q: Type
cct': forall a : A, C a -> Q
ppt': forall (b : B) (y : C (f b)),
cct' (f b) y = cct' (g b) (D b y)
b: B
y: C (f b)
ap
  (Wtil_ind (fun _ : Wtil A B f g C D => Q) cct'
     (fun (b : B) (y : C (f b)) =>
      transport_const (ppt b y) (cct' (f b) y) @
      ppt' b y)) (ppt b y) = ppt' b y
  eapply (cancelL (transport_const (ppt (C:=C) b y) _)).
A, B: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
Q: Type
cct': forall a : A, C a -> Q
ppt': forall (b : B) (y : C (f b)),
cct' (f b) y = cct' (g b) (D b y)
b: B
y: C (f b)
transport_const (ppt b y)
  (Wtil_ind (fun _ : Wtil A B f g C D => Q) cct'
     (fun (b : B) (y : C (f b)) =>
      transport_const (ppt b y) (cct' (f b) y) @
      ppt' b y) (cct (f b) y)) @
ap
  (Wtil_ind (fun _ : Wtil A B f g C D => Q) cct'
     (fun (b : B) (y : C (f b)) =>
      transport_const (ppt b y) (cct' (f b) y) @
      ppt' b y)) (ppt b y) =
transport_const (ppt b y)
  (Wtil_ind (fun _ : Wtil A B f g C D => Q) cct'
     (fun (b : B) (y : C (f b)) =>
      transport_const (ppt b y) (cct' (f b) y) @
      ppt' b y) (cct (f b) y)) @ ppt' b y
  refine ((apD_const
    (@Wtil_ind A B f g C D (fun _ => Q) cct' _) (ppt b y))^ @ _).
A, B: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
Q: Type
cct': forall a : A, C a -> Q
ppt': forall (b : B) (y : C (f b)),
cct' (f b) y = cct' (g b) (D b y)
b: B
y: C (f b)
apD
  (Wtil_ind (fun _ : Wtil A B f g C D => Q) cct'
     (fun (b : B) (y : C (f b)) =>
      transport_const (ppt b y) (cct' (f b) y) @
      ppt' b y)) (ppt b y) =
transport_const (ppt b y)
  (Wtil_ind (fun _ : Wtil A B f g C D => Q) cct'
     (fun (b : B) (y : C (f b)) =>
      transport_const (ppt b y) (cct' (f b) y) @
      ppt' b y) (cct (f b) y)) @ ppt' b y
  refine (Wtil_ind_beta_ppt (fun _ => Q) _ _ _ _).
Defined.



(** Now we define the fibration over it that we will be considering the total space of. *)

Section AssumeAxioms.
Context `{Univalence}.

Context {B A : Type} {f g : B -> A}.
Context {C : A -> Type} {D : forall b, C (f b) <~> C (g b)}.

Let W' := Coeq f g.

Let P : W' -> Type
  := Coeq_rec Type C (fun b => path_universe (D b)).



(** Now we give the total space the same structure as [Wtil]. *)

Let sWtil := { w:W' & P w }.

Let scct (a:A) (x:C a) : sWtil := (exist P (coeq a) x).

Let sppt (b:B) (y:C (f b)) : scct (f b) y = scct (g b) (D b y)
  := path_sigma' P (cglue b)
       (transport_path_universe' P (cglue b) (D b)
         (Coeq_rec_beta_cglue Type C (fun b0 => path_universe (D b0)) b) y).

(** Here is the dependent eliminator *)
Definition sWtil_ind (Q : sWtil -> Type)
  (scct' : forall a x, Q (scct a x))
  (sppt' : forall b y, (sppt b y) # (scct' (f b) y) = scct' (g b) (D b y))
  : forall w, Q w.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: sWtil -> Type
scct': forall (a : A) (x : C a), Q (scct a x)
sppt': forall (b : B) (y : C (f b)),
transport Q (sppt b y) (scct' (f b) y) =
scct' (g b) (D b y)
forall w : sWtil, Q w
Proof.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: sWtil -> Type
scct': forall (a : A) (x : C a), Q (scct a x)
sppt': forall (b : B) (y : C (f b)),
transport Q (sppt b y) (scct' (f b) y) =
scct' (g b) (D b y)
forall w : sWtil, Q w
  apply sig_ind.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: sWtil -> Type
scct': forall (a : A) (x : C a), Q (scct a x)
sppt': forall (b : B) (y : C (f b)),
transport Q (sppt b y) (scct' (f b) y) =
scct' (g b) (D b y)
forall (proj1 : W') (proj2 : P proj1),
Q (proj1; proj2)
  refine (Coeq_ind (fun w => forall x:P w, Q (w;x))
    (fun a x => scct' a x) _).
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: sWtil -> Type
scct': forall (a : A) (x : C a), Q (scct a x)
sppt': forall (b : B) (y : C (f b)),
transport Q (sppt b y) (scct' (f b) y) =
scct' (g b) (D b y)
forall b : B,
transport
  (fun w : Coeq f g => forall x : P w, Q (w; x))
  (cglue b) (fun x : P (coeq (f b)) => scct' (f b) x) =
(fun x : P (coeq (g b)) => scct' (g b) x)
  intros b.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: sWtil -> Type
scct': forall (a : A) (x : C a), Q (scct a x)
sppt': forall (b : B) (y : C (f b)),
transport Q (sppt b y) (scct' (f b) y) =
scct' (g b) (D b y)
b: B
transport
  (fun w : Coeq f g => forall x : P w, Q (w; x))
  (cglue b) (fun x : P (coeq (f b)) => scct' (f b) x) =
(fun x : P (coeq (g b)) => scct' (g b) x)
  apply (dpath_forall P (fun a b => Q (a;b)) _ _ (cglue b)
    (scct' (f b)) (scct' (g b))).
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: sWtil -> Type
scct': forall (a : A) (x : C a), Q (scct a x)
sppt': forall (b : B) (y : C (f b)),
transport Q (sppt b y) (scct' (f b) y) =
scct' (g b) (D b y)
b: B
forall y1 : P (coeq (f b)),
transportD P (fun (a : W') (b : P a) => Q (a; b))
  (cglue b) y1 (scct' (f b) y1) =
scct' (g b) (transport P (cglue b) y1)
  intros y.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: sWtil -> Type
scct': forall (a : A) (x : C a), Q (scct a x)
sppt': forall (b : B) (y : C (f b)),
transport Q (sppt b y) (scct' (f b) y) =
scct' (g b) (D b y)
b: B
y: P (coeq (f b))
transportD P (fun (a : W') (b : P a) => Q (a; b))
  (cglue b) y (scct' (f b) y) =
scct' (g b) (transport P (cglue b) y)
  set (q := transport_path_universe' P (cglue b) (D b)
    (Coeq_rec_beta_cglue Type C (fun b0 : B => path_universe (D b0)) b) y).
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: sWtil -> Type
scct': forall (a : A) (x : C a), Q (scct a x)
sppt': forall (b : B) (y : C (f b)),
transport Q (sppt b y) (scct' (f b) y) =
scct' (g b) (D b y)
b: B
y: P (coeq (f b))
q:= transport_path_universe' P 
  (cglue b) (D b)
  (Coeq_rec_beta_cglue Type C
     (fun b0 : B => path_universe (D b0)) b) y: transport P (cglue b) y = D b y
transportD P (fun (a : W') (b : P a) => Q (a; b))
  (cglue b) y (scct' (f b) y) =
scct' (g b) (transport P (cglue b) y)
  rewrite transportD_is_transport.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: sWtil -> Type
scct': forall (a : A) (x : C a), Q (scct a x)
sppt': forall (b : B) (y : C (f b)),
transport Q (sppt b y) (scct' (f b) y) =
scct' (g b) (D b y)
b: B
y: P (coeq (f b))
q:= transport_path_universe' P 
  (cglue b) (D b)
  (Coeq_rec_beta_cglue Type C
     (fun b0 : B => path_universe (D b0)) b) y: transport P (cglue b) y = D b y
transport Q (path_sigma' P (cglue b) 1)
  (scct' (f b) y) =
scct' (g b) (transport P (cglue b) y)
  refine (_ @ apD (scct' (g b)) q^).
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: sWtil -> Type
scct': forall (a : A) (x : C a), Q (scct a x)
sppt': forall (b : B) (y : C (f b)),
transport Q (sppt b y) (scct' (f b) y) =
scct' (g b) (D b y)
b: B
y: P (coeq (f b))
q:= transport_path_universe' P 
  (cglue b) (D b)
  (Coeq_rec_beta_cglue Type C
     (fun b0 : B => path_universe (D b0)) b) y: transport P (cglue b) y = D b y
transport Q (path_sigma' P (cglue b) 1)
  (scct' (f b) y) =
transport (fun x : C (g b) => Q (scct (g b) x)) q^
  (scct' (g b) (D b y))
  refine (moveL_transport_V (fun x => Q (scct (g b) x)) q _ _ _).
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: sWtil -> Type
scct': forall (a : A) (x : C a), Q (scct a x)
sppt': forall (b : B) (y : C (f b)),
transport Q (sppt b y) (scct' (f b) y) =
scct' (g b) (D b y)
b: B
y: P (coeq (f b))
q:= transport_path_universe' P 
  (cglue b) (D b)
  (Coeq_rec_beta_cglue Type C
     (fun b0 : B => path_universe (D b0)) b) y: transport P (cglue b) y = D b y
transport (fun x : C (g b) => Q (scct (g b) x)) q
  (transport Q (path_sigma' P (cglue b) 1)
     (scct' (f b) y)) = scct' (g b) (D b y)
  rewrite transport_compose, <- transport_pp.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: sWtil -> Type
scct': forall (a : A) (x : C a), Q (scct a x)
sppt': forall (b : B) (y : C (f b)),
transport Q (sppt b y) (scct' (f b) y) =
scct' (g b) (D b y)
b: B
y: P (coeq (f b))
q:= transport_path_universe' P 
  (cglue b) (D b)
  (Coeq_rec_beta_cglue Type C
     (fun b0 : B => path_universe (D b0)) b) y: transport P (cglue b) y = D b y
transport Q
  (path_sigma' P (cglue b) 1 @ ap (scct (g b)) q)
  (scct' (f b) y) = scct' (g b) (D b y)
  refine (_ @ sppt' b y).
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: sWtil -> Type
scct': forall (a : A) (x : C a), Q (scct a x)
sppt': forall (b : B) (y : C (f b)),
transport Q (sppt b y) (scct' (f b) y) =
scct' (g b) (D b y)
b: B
y: P (coeq (f b))
q:= transport_path_universe' P 
  (cglue b) (D b)
  (Coeq_rec_beta_cglue Type C
     (fun b0 : B => path_universe (D b0)) b) y: transport P (cglue b) y = D b y
transport Q
  (path_sigma' P (cglue b) 1 @ ap (scct (g b)) q)
  (scct' (f b) y) =
transport Q (sppt b y) (scct' (f b) y)
  apply ap10, ap.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: sWtil -> Type
scct': forall (a : A) (x : C a), Q (scct a x)
sppt': forall (b : B) (y : C (f b)),
transport Q (sppt b y) (scct' (f b) y) =
scct' (g b) (D b y)
b: B
y: P (coeq (f b))
q:= transport_path_universe' P 
  (cglue b) (D b)
  (Coeq_rec_beta_cglue Type C
     (fun b0 : B => path_universe (D b0)) b) y: transport P (cglue b) y = D b y
path_sigma' P (cglue b) 1 @ ap (scct (g b)) q =
sppt b y
  refine (whiskerL _ (ap_exist P (coeq (g b)) _ _ q) @ _).
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: sWtil -> Type
scct': forall (a : A) (x : C a), Q (scct a x)
sppt': forall (b : B) (y : C (f b)),
transport Q (sppt b y) (scct' (f b) y) =
scct' (g b) (D b y)
b: B
y: P (coeq (f b))
q:= transport_path_universe' P 
  (cglue b) (D b)
  (Coeq_rec_beta_cglue Type C
     (fun b0 : B => path_universe (D b0)) b) y: transport P (cglue b) y = D b y
path_sigma' P (cglue b) 1 @ path_sigma' P 1 q =
sppt b y
  exact ((path_sigma_p1_1p' _ _ _)^).
Defined.

(** The eliminator computes on the point constructor. *)
Definition sWtil_ind_beta_cct (Q : sWtil -> Type)
  (scct' : forall a x, Q (scct a x))
  (sppt' : forall b y, (sppt b y) # (scct' (f b) y) = scct' (g b) (D b y))
  (a:A) (x:C a)
  : sWtil_ind Q scct' sppt' (scct a x) = scct' a x
  := 1.

(** This would be its propositional computation rule on the path constructor... *)
(**
<<
Definition sWtil_ind_beta_ppt (Q : sWtil -> Type)
  (scct' : forall a x, Q (scct a x))
  (sppt' : forall b y, (sppt b y) # (scct' (f b) y) = scct' (g b) (D b y))
  (b:B) (y:C (f b))
  : apD (sWtil_ind Q scct' sppt') (sppt b y) = sppt' b y.
Proof.
  unfold sWtil_ind.
  (** ... but it's a doozy! *)
Abort.
>>
*)

(** Fortunately, it turns out to be enough to have the computation rule for the *non-dependent* eliminator! *)

(** We could define that in terms of the dependent one, as usual...
<<
Definition sWtil_rec (P : Type)
  (scct' : forall a (x : C a), P)
  (sppt' : forall b (y : C (f b)), scct' (f b) y = scct' (g b) (D b y))
  : sWtil -> P
  := sWtil_ind (fun _ => P) scct' (fun b y => transport_const _ _ @ sppt' b y).
>>
*)

(** ...but if we define it diindly, then it's easier to reason about. *)
Definition sWtil_rec (Q : Type)
  (scct' : forall a (x : C a), Q)
  (sppt' : forall b (y : C (f b)), scct' (f b) y = scct' (g b) (D b y))
  : sWtil -> Q.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
sWtil -> Q
Proof.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
sWtil -> Q
  apply sig_ind.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
forall proj1 : W', P proj1 -> Q
  refine (Coeq_ind (fun w => P w -> Q) (fun a x => scct' a x) _).
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
forall b : B,
transport (fun w : Coeq f g => P w -> Q) (cglue b)
  (fun x : P (coeq (f b)) => scct' (f b) x) =
(fun x : P (coeq (g b)) => scct' (g b) x)
  intros b.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
b: B
transport (fun w : Coeq f g => P w -> Q) (cglue b)
  (fun x : P (coeq (f b)) => scct' (f b) x) =
(fun x : P (coeq (g b)) => scct' (g b) x)
  refine (dpath_arrow P (fun _ => Q) _ _ _ _).
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
b: B
forall y1 : P (coeq (f b)),
transport (fun _ : W' => Q) (cglue b) (scct' (f b) y1) =
scct' (g b) (transport P (cglue b) y1)
  intros y.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
b: B
y: P (coeq (f b))
transport (fun _ : W' => Q) (cglue b) (scct' (f b) y) =
scct' (g b) (transport P (cglue b) y)
  refine (transport_const _ _ @ _).
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
b: B
y: P (coeq (f b))
scct' (f b) y = scct' (g b) (transport P (cglue b) y)
  refine (sppt' b _ @ ap _ _).
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
b: B
y: P (coeq (f b))
D b y = transport P (cglue b) y
  refine ((transport_path_universe' P (cglue b) (D b) _ _)^).
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
b: B
y: P (coeq (f b))
ap P (cglue b) = path_universe (D b)
  exact (Coeq_rec_beta_cglue _ _ _ _).
Defined.

Open Scope long_path_scope.

Definition sWtil_rec_beta_ppt (Q : Type)
  (scct' : forall a (x : C a), Q)
  (sppt' : forall b (y : C (f b)), scct' (f b) y = scct' (g b) (D b y))
  (b:B) (y: C (f b))
  : ap (sWtil_rec Q scct' sppt') (sppt b y) = sppt' b y.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
b: B
y: C (f b)
ap (sWtil_rec Q scct' sppt') (sppt b y) = sppt' b y
Proof.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
b: B
y: C (f b)
ap (sWtil_rec Q scct' sppt') (sppt b y) = sppt' b y
  unfold sWtil_rec, sppt.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
b: B
y: C (f b)
ap
  (sig_ind (fun _ : {w : W' & P w} => Q)
     (Coeq_ind (fun w : Coeq f g => P w -> Q)
        (fun (a : A) (x : P (coeq a)) => scct' a x)
        (fun b : B =>
         dpath_arrow P (fun _ : W' => Q) (cglue b)
           (fun x : P (coeq (f b)) => scct' (f b) x)
           (fun x : P (coeq (g b)) => scct' (g b) x)
           (fun y : P (coeq (f b)) =>
            transport_const (cglue b) (scct' (f b) y)
            @' (sppt' b y
                @' ap (scct' (g b))
                     (transport_path_universe' P
                        (cglue b) (D b)
                        (Coeq_rec_beta_cglue Type C
                           (fun b0 : B =>
                            path_universe (D b0)) b) y)^)))))
  (path_sigma' P (cglue b)
     (transport_path_universe' P (cglue b) (D b)
        (Coeq_rec_beta_cglue Type C
           (fun b0 : B => path_universe (D b0)) b) y)) =
sppt' b y
  refine (@ap_sig_rec_path_sigma W' P Q _ _ (cglue b) _ _ _ _ @ _); simpl.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
b: B
y: C (f b)
(transport_const (cglue b) (scct' (f b) y))^
@' (ap
      (fun x : C (f b) =>
       transport (fun _ : W' => Q) (cglue b)
         (scct' (f b) x)) (transport_Vp P (cglue b) y))^
@' (transport_arrow (cglue b)
      (fun x : C (f b) => scct' (f b) x)
      (transport P (cglue b) y))^
@' ap10
     (apD
        (Coeq_ind (fun w : Coeq f g => P w -> Q)
           (fun (a : A) (x : C a) => scct' a x)
           (fun b : B =>
            dpath_arrow P (fun _ : W' => Q) (cglue b)
              (fun x : C (f b) => scct' (f b) x)
              (fun x : C (g b) => scct' (g b) x)
              (fun y : C (f b) =>
               transport_const (cglue b)
                 (scct' (f b) y)
               @' (sppt' b y
                   @' ap (scct' (g b))
                        (transport_path_universe' P
                           (cglue b) (D b)
                           (Coeq_rec_beta_cglue Type C
                              (fun b0 : B =>
                               path_universe (D b0)) b)
                           y)^)))) (cglue b))
     (transport P (cglue b) y)
@' ap (fun x : C (g b) => scct' (g b) x)
     (transport_path_universe' P (cglue b) (D b)
        (Coeq_rec_beta_cglue Type C
           (fun b0 : B => path_universe (D b0)) b) y) =
sppt' b y
  rewrite (@Coeq_ind_beta_cglue B A f g).
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
b: B
y: C (f b)
(transport_const (cglue b) (scct' (f b) y))^
@' (ap
      (fun x : C (f b) =>
       transport (fun _ : W' => Q) (cglue b)
         (scct' (f b) x)) (transport_Vp P (cglue b) y))^
@' (transport_arrow (cglue b)
      (fun x : C (f b) => scct' (f b) x)
      (transport P (cglue b) y))^
@' ap10
     (dpath_arrow P (fun _ : W' => Q) (cglue b)
        (fun x : C (f b) => scct' (f b) x)
        (fun x : C (g b) => scct' (g b) x)
        (fun y : C (f b) =>
         transport_const (cglue b) (scct' (f b) y)
         @' (sppt' b y
             @' ap (scct' (g b))
                  (transport_path_universe' P
                     (cglue b) (D b)
                     (Coeq_rec_beta_cglue Type C
                        (fun b : B =>
                         path_universe (D b)) b) y)^)))
     (transport P (cglue b) y)
@' ap (fun x : C (g b) => scct' (g b) x)
     (transport_path_universe' P (cglue b) (D b)
        (Coeq_rec_beta_cglue Type C
           (fun b0 : B => path_universe (D b0)) b) y) =
sppt' b y
  rewrite (ap10_dpath_arrow P (fun _ => Q) (cglue b) _ _ _ y).
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
b: B
y: C (f b)
(transport_const (cglue b) (scct' (f b) y))^
@' (ap
      (fun x : C (f b) =>
       transport (fun _ : W' => Q) (cglue b)
         (scct' (f b) x)) (transport_Vp P (cglue b) y))^
@' (transport_arrow (cglue b)
      (fun x : C (f b) => scct' (f b) x)
      (transport P (cglue b) y))^
@' (transport_arrow (cglue b)
      (fun x : C (f b) => scct' (f b) x)
      (transport P (cglue b) y)
    @' ap
         (fun x : P (coeq (f b)) =>
          transport (fun _ : W' => Q) (cglue b)
            (scct' (f b) x))
         (transport_Vp P (cglue b) y)
    @' (transport_const (cglue b) (scct' (f b) y)
        @' (sppt' b y
            @' ap (scct' (g b))
                 (transport_path_universe' P (cglue b)
                    (D b)
                    (Coeq_rec_beta_cglue Type C
                       (fun b : B =>
                        path_universe (D b)) b) y)^)))
@' ap (fun x : C (g b) => scct' (g b) x)
     (transport_path_universe' P (cglue b) (D b)
        (Coeq_rec_beta_cglue Type C
           (fun b0 : B => path_universe (D b0)) b) y) =
sppt' b y
  repeat rewrite concat_p_pp.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
b: B
y: C (f b)
(transport_const (cglue b) (scct' (f b) y))^
@' (ap
      (fun x : C (f b) =>
       transport (fun _ : W' => Q) (cglue b)
         (scct' (f b) x)) (transport_Vp P (cglue b) y))^
@' (transport_arrow (cglue b)
      (fun x : C (f b) => scct' (f b) x)
      (transport P (cglue b) y))^
@' transport_arrow (cglue b)
     (fun x : C (f b) => scct' (f b) x)
     (transport P (cglue b) y)
@' ap
     (fun x : P (coeq (f b)) =>
      transport (fun _ : W' => Q) (cglue b)
        (scct' (f b) x)) (transport_Vp P (cglue b) y)
@' transport_const (cglue b) (scct' (f b) y)
@' sppt' b y
@' ap (scct' (g b))
     (transport_path_universe' P (cglue b) (D b)
        (Coeq_rec_beta_cglue Type C
           (fun b : B => path_universe (D b)) b) y)^
@' ap (fun x : C (g b) => scct' (g b) x)
     (transport_path_universe' P (cglue b) (D b)
        (Coeq_rec_beta_cglue Type C
           (fun b0 : B => path_universe (D b0)) b) y) =
sppt' b y
  (** Now everything cancels! *)
  rewrite ap_V, concat_pV_p, concat_pV_p, concat_pV_p, concat_Vp.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Q: Type
scct': forall a : A, C a -> Q
sppt': forall (b : B) (y : C (f b)),
scct' (f b) y = scct' (g b) (D b y)
b: B
y: C (f b)
1
@' sppt' b y = sppt' b y
  by apply concat_1p.
Qed.

Close Scope long_path_scope.

(** Woot! *)
Definition equiv_flattening : Wtil A B f g C D <~> sWtil.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Wtil A B f g C D <~> sWtil
Proof.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
Wtil A B f g C D <~> sWtil
  (** The maps back and forth are obtained easily from the non-dependent eliminators. *)
  refine (equiv_adjointify
    (Wtil_rec _ scct sppt)
    (sWtil_rec _ cct ppt)
    _ _).
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
(fun x : sWtil =>
 Wtil_rec sWtil scct sppt
   (sWtil_rec (Wtil A B f g C D) cct ppt x)) == idmap
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
(fun x : Wtil A B f g C D =>
 sWtil_rec (Wtil A B f g C D) cct ppt
   (Wtil_rec sWtil scct sppt x)) == idmap
  (** The two homotopies are completely symmetrical, using the *dependent* eliminators, but only the computation rules for the non-dependent ones. *)
  -
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
(fun x : sWtil =>
 Wtil_rec sWtil scct sppt
   (sWtil_rec (Wtil A B f g C D) cct ppt x)) == idmap refine (sWtil_ind _ (fun a x => 1) _).
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
forall (b : B) (y : C (f b)),
transport
  (fun w : sWtil =>
   Wtil_rec sWtil scct sppt
     (sWtil_rec (Wtil A B f g C D) cct ppt w) = w)
  (sppt b y) 1 = 1 intros b y.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
b: B
y: C (f b)
transport
  (fun w : sWtil =>
   Wtil_rec sWtil scct sppt
     (sWtil_rec (Wtil A B f g C D) cct ppt w) = w)
  (sppt b y) 1 = 1
    apply dpath_path_FFlr.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
b: B
y: C (f b)
1 @ sppt b y =
ap (Wtil_rec sWtil scct sppt)
  (ap (sWtil_rec (Wtil A B f g C D) cct ppt)
     (sppt b y)) @ 1
    rewrite concat_1p, concat_p1.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
b: B
y: C (f b)
sppt b y =
ap (Wtil_rec sWtil scct sppt)
  (ap (sWtil_rec (Wtil A B f g C D) cct ppt)
     (sppt b y))
    rewrite sWtil_rec_beta_ppt.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
b: B
y: C (f b)
sppt b y = ap (Wtil_rec sWtil scct sppt) (ppt b y)
      by symmetry; apply (@Wtil_rec_beta_ppt A B f g C D).
  -
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
(fun x : Wtil A B f g C D =>
 sWtil_rec (Wtil A B f g C D) cct ppt
   (Wtil_rec sWtil scct sppt x)) == idmap refine (Wtil_ind _ (fun a x => 1) _).
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
forall (b : B) (y : C (f b)),
transport
  (fun w : Wtil A B f g C D =>
   sWtil_rec (Wtil A B f g C D) cct ppt
     (Wtil_rec sWtil scct sppt w) = w) (ppt b y) 1 = 1 intros b y.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
b: B
y: C (f b)
transport
  (fun w : Wtil A B f g C D =>
   sWtil_rec (Wtil A B f g C D) cct ppt
     (Wtil_rec sWtil scct sppt w) = w) (ppt b y) 1 = 1
    apply dpath_path_FFlr.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
b: B
y: C (f b)
1 @ ppt b y =
ap (sWtil_rec (Wtil A B f g C D) cct ppt)
  (ap (Wtil_rec sWtil scct sppt) (ppt b y)) @ 1
    rewrite concat_1p, concat_p1.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
b: B
y: C (f b)
ppt b y =
ap (sWtil_rec (Wtil A B f g C D) cct ppt)
  (ap (Wtil_rec sWtil scct sppt) (ppt b y))
    rewrite Wtil_rec_beta_ppt.
H: Univalence
B, A: Type
f, g: B -> A
C: A -> Type
D: forall b : B, C (f b) <~> C (g b)
W':= Coeq f g: Type
P:= Coeq_rec Type C (fun b : B => path_universe (D b)): W' -> Type
sWtil:= {w : W' & P w}: Type
scct:= fun (a : A) (x : C a) => (coeq a; x): forall a : A, C a -> sWtil
sppt:= fun (b : B) (y : C (f b)) =>
path_sigma' P (cglue b)
  (transport_path_universe' P 
     (cglue b) (D b)
     (Coeq_rec_beta_cglue Type C
        (fun b0 : B => path_universe (D b0)) b)
     y): forall (b : B) (y : C (f b)),
scct (f b) y = scct (g b) (D b y)
b: B
y: C (f b)
ppt b y =
ap (sWtil_rec (Wtil A B f g C D) cct ppt) (sppt b y)
      by symmetry; apply sWtil_rec_beta_ppt.
Defined.

End AssumeAxioms.