Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod.
Require Import Colimits.GraphQuotient.
Require Import Homotopy.IdentitySystems.

Local Open Scope path_scope.

(** * Homotopy coequalizers *)

(** ** Definition *)

Definition Coeq@{i j u} {B : Type@{i}} {A : Type@{j}} (f g : B -> A) : Type@{u}
  := GraphQuotient@{i j u} (fun a b => {x : B & (f x = a) * (g x = b)}).

Definition coeq {B A f g} (a : A) : @Coeq B A f g := gq a.
Definition cglue {B A f g} b : @coeq B A f g (f b) = coeq (g b)
  := gqglue (b; (idpath,idpath)).

Arguments Coeq : simpl never.
Arguments coeq : simpl never.
Arguments cglue : simpl never.

Definition Coeq_ind {B A f g} (P : @Coeq B A f g -> Type)
  (coeq' : forall a, P (coeq a))
  (cglue' : forall b, (cglue b) # (coeq' (f b)) = coeq' (g b))
  : forall w, P w.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
coeq': forall a : A, P (coeq a)
cglue': forall b : B,
transport P (cglue b) (coeq' (f b)) =
coeq' (g b)
forall w : Coeq f g, P w
Proof.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
coeq': forall a : A, P (coeq a)
cglue': forall b : B,
transport P (cglue b) (coeq' (f b)) =
coeq' (g b)
forall w : Coeq f g, P w
  rapply GraphQuotient_ind.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
coeq': forall a : A, P (coeq a)
cglue': forall b : B,
transport P (cglue b) (coeq' (f b)) =
coeq' (g b)
forall (a b : A)
(s : {x : B & (f x = a) * (g x = b)}),
transport P (gqglue s) (?Goal a) = ?Goal b
  intros a b [x [[] []]].
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
coeq': forall a : A, P (coeq a)
cglue': forall b : B,
transport P (cglue b) (coeq' (f b)) =
coeq' (g b)
a, b: A
x: B
transport P (gqglue (x; (1, 1))) (?Goal (f x)) =
?Goal (g x)
  exact (cglue' x).
Defined.

Lemma Coeq_ind_beta_cglue {B A f g} (P : @Coeq B A f g -> Type)
  (coeq' : forall a, P (coeq a))
  (cglue' : forall b, (cglue b) # (coeq' (f b)) = coeq' (g b)) (b:B)
  : apD (Coeq_ind P coeq' cglue') (cglue b) = cglue' b.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
coeq': forall a : A, P (coeq a)
cglue': forall b : B,
transport P (cglue b) (coeq' (f b)) =
coeq' (g b)
b: B
apD (Coeq_ind P coeq' cglue') (cglue b) = cglue' b
Proof.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
coeq': forall a : A, P (coeq a)
cglue': forall b : B,
transport P (cglue b) (coeq' (f b)) =
coeq' (g b)
b: B
apD (Coeq_ind P coeq' cglue') (cglue b) = cglue' b
  rapply GraphQuotient_ind_beta_gqglue.
Defined.

Definition Coeq_rec {B A f g} (P : Type) (coeq' : A -> P)
  (cglue' : forall b, coeq' (f b) = coeq' (g b))
  : @Coeq B A f g -> P.
B, A: Type
f, g: B -> A
P: Type
coeq': A -> P
cglue': forall b : B, coeq' (f b) = coeq' (g b)
Coeq f g -> P
Proof.
B, A: Type
f, g: B -> A
P: Type
coeq': A -> P
cglue': forall b : B, coeq' (f b) = coeq' (g b)
Coeq f g -> P
  rapply GraphQuotient_rec.
B, A: Type
f, g: B -> A
P: Type
coeq': A -> P
cglue': forall b : B, coeq' (f b) = coeq' (g b)
forall a b : A,
{x : B & (f x = a) * (g x = b)} -> ?Goal a = ?Goal b
  intros a b [x [[] []]].
B, A: Type
f, g: B -> A
P: Type
coeq': A -> P
cglue': forall b : B, coeq' (f b) = coeq' (g b)
a, b: A
x: B
?Goal (f x) = ?Goal (g x)
  exact (cglue' x).
Defined.

Definition Coeq_rec_beta_cglue {B A f g} (P : Type) (coeq' : A -> P)
  (cglue' : forall b:B, coeq' (f b) = coeq' (g b)) (b:B)
  : ap (Coeq_rec P coeq' cglue') (cglue b) = cglue' b.
B, A: Type
f, g: B -> A
P: Type
coeq': A -> P
cglue': forall b : B, coeq' (f b) = coeq' (g b)
b: B
ap (Coeq_rec P coeq' cglue') (cglue b) = cglue' b
Proof.
B, A: Type
f, g: B -> A
P: Type
coeq': A -> P
cglue': forall b : B, coeq' (f b) = coeq' (g b)
b: B
ap (Coeq_rec P coeq' cglue') (cglue b) = cglue' b
  rapply GraphQuotient_rec_beta_gqglue.
Defined.

Definition Coeq_ind_hprop {B A f g} (P : @Coeq B A f g -> Type)
  `{forall x, IsHProp (P x)}
  (i : forall a, P (coeq a))
  : forall x, P x.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
H: forall x : Coeq f g, IsHProp (P x)
i: forall a : A, P (coeq a)
forall x : Coeq f g, P x
Proof.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
H: forall x : Coeq f g, IsHProp (P x)
i: forall a : A, P (coeq a)
forall x : Coeq f g, P x
  snapply Coeq_ind.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
H: forall x : Coeq f g, IsHProp (P x)
i: forall a : A, P (coeq a)
forall a : A, P (coeq a)
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
H: forall x : Coeq f g, IsHProp (P x)
i: forall a : A, P (coeq a)
forall b : B,
transport P (cglue b) (?coeq' (f b)) = ?coeq' (g b)
  1: exact i.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
H: forall x : Coeq f g, IsHProp (P x)
i: forall a : A, P (coeq a)
forall b : B,
transport P (cglue b) (i (f b)) = i (g b)
  intros b.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
H: forall x : Coeq f g, IsHProp (P x)
i: forall a : A, P (coeq a)
b: B
transport P (cglue b) (i (f b)) = i (g b)
  rapply path_ishprop.
Defined.

Definition Coeq_ind_eta_homotopic {B A f g} {P : @Coeq B A f g -> Type}
  (h : forall w : Coeq f g, P w)
  : h == Coeq_ind P (h o coeq) (fun b => apD h (cglue b)).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall w : Coeq f g, P w
h ==
Coeq_ind P (h o coeq) (fun b : B => apD h (cglue b))
Proof.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall w : Coeq f g, P w
h ==
Coeq_ind P (h o coeq) (fun b : B => apD h (cglue b))
  unfold pointwise_paths.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall w : Coeq f g, P w
forall x : Coeq f g,
h x =
Coeq_ind P (fun x0 : A => h (coeq x0))
  (fun b : B => apD h (cglue b)) x
  napply (Coeq_ind _ (fun _ => 1)).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall w : Coeq f g, P w
forall b : B,
transport
  (fun w : Coeq f g =>
   h w =
   Coeq_ind P (fun x : A => h (coeq x))
     (fun b0 : B => apD h (cglue b0)) w) (cglue b) 1 =
1
  intros b.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall w : Coeq f g, P w
b: B
transport
  (fun w : Coeq f g =>
   h w =
   Coeq_ind P (fun x : A => h (coeq x))
     (fun b : B => apD h (cglue b)) w) (cglue b) 1 = 1
  lhs napply transport_paths_FlFr_D.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall w : Coeq f g, P w
b: B
((apD h (cglue b))^ @ ap (transport P (cglue b)) 1) @
apD
  (Coeq_ind P (fun x : A => h (coeq x))
     (fun b : B => apD h (cglue b))) (cglue b) = 1
  lhs napply (whiskerL _ (Coeq_ind_beta_cglue _ _ _ _)).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall w : Coeq f g, P w
b: B
((apD h (cglue b))^ @ ap (transport P (cglue b)) 1) @
apD h (cglue b) = 1
  lhs napply (whiskerR (concat_p1 _)).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall w : Coeq f g, P w
b: B
(apD h (cglue b))^ @ apD h (cglue b) = 1
  napply concat_Vp.
Defined.

Definition Coeq_rec_eta_homotopic {B A f g} {P : Type} (h : @Coeq B A f g -> P)
  : h == Coeq_rec P (h o coeq) (fun b => ap h (cglue b)).
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
h ==
Coeq_rec P (h o coeq) (fun b : B => ap h (cglue b))
Proof.
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
h ==
Coeq_rec P (h o coeq) (fun b : B => ap h (cglue b))
  unfold pointwise_paths.
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
forall x : Coeq f g,
h x =
Coeq_rec P (fun x0 : A => h (coeq x0))
  (fun b : B => ap h (cglue b)) x
  napply (Coeq_ind _ (fun _ => 1)).
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
forall b : B,
transport
  (fun w : Coeq f g =>
   h w =
   Coeq_rec P (fun x : A => h (coeq x))
     (fun b0 : B => ap h (cglue b0)) w) (cglue b) 1 =
1
  intros b.
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
b: B
transport
  (fun w : Coeq f g =>
   h w =
   Coeq_rec P (fun x : A => h (coeq x))
     (fun b : B => ap h (cglue b)) w) (cglue b) 1 = 1
  transport_paths FlFr.
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
b: B
ap h (cglue b) @ 1 =
1 @
ap
  (Coeq_rec P (fun x : A => h (coeq x))
     (fun b : B => ap h (cglue b))) (cglue b)
  apply equiv_p1_1q.
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
b: B
ap h (cglue b) =
ap
  (Coeq_rec P (fun x : A => h (coeq x))
     (fun b : B => ap h (cglue b))) (cglue b)
  symmetry; napply Coeq_rec_beta_cglue.
Defined.

Definition Coeq_ind_eta `{Funext}
  {B A f g} {P : @Coeq B A f g -> Type} (h : forall w : Coeq f g, P w)
  : h = Coeq_ind P (h o coeq) (fun b => apD h (cglue b))
  := path_forall _ _ (Coeq_ind_eta_homotopic h).

Definition Coeq_rec_eta `{Funext}
  {B A f g} {P : Type} (h : @Coeq B A f g -> P)
  : h = Coeq_rec P (h o coeq) (fun b => ap h (cglue b))
  := path_forall _ _ (Coeq_rec_eta_homotopic h).

Definition Coeq_ind_homotopy {B A f g} (P : @Coeq B A f g -> Type)
  {m n : forall a, P (coeq a)} (u : m == n)
  {r : forall b, (cglue b) # (m (f b)) = m (g b)}
  {s : forall b, (cglue b) # (n (f b)) = n (g b)}
  (p : forall b, ap (transport P (cglue b)) (u (f b)) @ (s b) = r b @ u (g b))
  : Coeq_ind P m r == Coeq_ind P n s.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
m, n: forall a : A, P (coeq a)
u: m == n
r: forall b : B,
transport P (cglue b) (m (f b)) = m (g b)
s: forall b : B,
transport P (cglue b) (n (f b)) = n (g b)
p: forall b : B,
ap (transport P (cglue b)) (u (f b)) @ s b =
r b @ u (g b)
Coeq_ind P m r == Coeq_ind P n s
Proof.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
m, n: forall a : A, P (coeq a)
u: m == n
r: forall b : B,
transport P (cglue b) (m (f b)) = m (g b)
s: forall b : B,
transport P (cglue b) (n (f b)) = n (g b)
p: forall b : B,
ap (transport P (cglue b)) (u (f b)) @ s b =
r b @ u (g b)
Coeq_ind P m r == Coeq_ind P n s
  unfold pointwise_paths.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
m, n: forall a : A, P (coeq a)
u: m == n
r: forall b : B,
transport P (cglue b) (m (f b)) = m (g b)
s: forall b : B,
transport P (cglue b) (n (f b)) = n (g b)
p: forall b : B,
ap (transport P (cglue b)) (u (f b)) @ s b =
r b @ u (g b)
forall x : Coeq f g,
Coeq_ind P m r x = Coeq_ind P n s x
  napply Coeq_ind; intros b.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
m, n: forall a : A, P (coeq a)
u: m == n
r: forall b : B,
transport P (cglue b) (m (f b)) = m (g b)
s: forall b : B,
transport P (cglue b) (n (f b)) = n (g b)
p: forall b : B,
ap (transport P (cglue b)) (u (f b)) @ s b =
r b @ u (g b)
b: B
transport
  (fun w : Coeq f g =>
   Coeq_ind P m r w = Coeq_ind P n s w) (cglue b)
  (?Goal (f b)) = ?Goal (g b)
  lhs napply (transport_paths_FlFr_D (f:=Coeq_ind P m r) (g:=Coeq_ind P n s)).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
m, n: forall a : A, P (coeq a)
u: m == n
r: forall b : B,
transport P (cglue b) (m (f b)) = m (g b)
s: forall b : B,
transport P (cglue b) (n (f b)) = n (g b)
p: forall b : B,
ap (transport P (cglue b)) (u (f b)) @ s b =
r b @ u (g b)
b: B
((apD (Coeq_ind P m r) (cglue b))^ @
 ap (transport P (cglue b)) (?Goal (f b))) @
apD (Coeq_ind P n s) (cglue b) = ?Goal (g b)
  lhs napply (whiskerL _ (Coeq_ind_beta_cglue P n s b)).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
m, n: forall a : A, P (coeq a)
u: m == n
r: forall b : B,
transport P (cglue b) (m (f b)) = m (g b)
s: forall b : B,
transport P (cglue b) (n (f b)) = n (g b)
p: forall b : B,
ap (transport P (cglue b)) (u (f b)) @ s b =
r b @ u (g b)
b: B
((apD (Coeq_ind P m r) (cglue b))^ @
 ap (transport P (cglue b)) (?Goal (f b))) @ s b =
?Goal (g b)
  lhs napply (whiskerR (whiskerR (ap inverse (Coeq_ind_beta_cglue P m r b)) _)).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
m, n: forall a : A, P (coeq a)
u: m == n
r: forall b : B,
transport P (cglue b) (m (f b)) = m (g b)
s: forall b : B,
transport P (cglue b) (n (f b)) = n (g b)
p: forall b : B,
ap (transport P (cglue b)) (u (f b)) @ s b =
r b @ u (g b)
b: B
((r b)^ @ ap (transport P (cglue b)) (?Goal (f b))) @
s b = ?Goal (g b)
  lhs napply concat_pp_p; napply moveR_Mp.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
m, n: forall a : A, P (coeq a)
u: m == n
r: forall b : B,
transport P (cglue b) (m (f b)) = m (g b)
s: forall b : B,
transport P (cglue b) (n (f b)) = n (g b)
p: forall b : B,
ap (transport P (cglue b)) (u (f b)) @ s b =
r b @ u (g b)
b: B
ap (transport P (cglue b)) (?Goal (f b)) @ s b =
((r b)^)^ @ ?Goal (g b)
  rhs napply (whiskerR (inv_V _)).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
m, n: forall a : A, P (coeq a)
u: m == n
r: forall b : B,
transport P (cglue b) (m (f b)) = m (g b)
s: forall b : B,
transport P (cglue b) (n (f b)) = n (g b)
p: forall b : B,
ap (transport P (cglue b)) (u (f b)) @ s b =
r b @ u (g b)
b: B
ap (transport P (cglue b)) (?Goal (f b)) @ s b =
r b @ ?Goal (g b)
  exact (p b).
Defined.

(** ** Universal property *)
(** See Colimits/CoeqUnivProp.v for a similar universal property without [Funext]. *)

Definition Coeq_unrec {B A} (f g : B -> A) {P}
  (h : Coeq f g -> P)
  : {k : A -> P & k o f == k o g}.
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
{k : A -> P & k o f == k o g}
Proof.
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
{k : A -> P & k o f == k o g}
  exists (h o coeq).
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
(fun x : B => h (coeq (f x))) ==
(fun x : B => h (coeq (g x)))
  intros b.
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
b: B
h (coeq (f b)) = h (coeq (g b)) exact (ap h (cglue b)).
Defined.

Definition isequiv_Coeq_rec `{Funext} {B A} (f g : B -> A) P
  : IsEquiv (fun p : {h : A -> P & h o f == h o g} => Coeq_rec P p.1 p.2).
H: Funext
B, A: Type
f, g: B -> A
P: Type
IsEquiv
  (fun p : {h : A -> P & h o f == h o g} =>
   Coeq_rec P p.1 p.2)
Proof.
H: Funext
B, A: Type
f, g: B -> A
P: Type
IsEquiv
  (fun p : {h : A -> P & h o f == h o g} =>
   Coeq_rec P p.1 p.2)
  srapply (isequiv_adjointify _ (Coeq_unrec f g)).
H: Funext
B, A: Type
f, g: B -> A
P: Type
(fun p : {h : A -> P & h o f == h o g} =>
 Coeq_rec P p.1 p.2) o Coeq_unrec f g == idmap
H: Funext
B, A: Type
f, g: B -> A
P: Type
Coeq_unrec f g
o (fun p : {h : A -> P & h o f == h o g} =>
   Coeq_rec P p.1 p.2) == idmap
  -
H: Funext
B, A: Type
f, g: B -> A
P: Type
(fun p : {h : A -> P & h o f == h o g} =>
 Coeq_rec P p.1 p.2) o Coeq_unrec f g == idmap intros h.
H: Funext
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
Coeq_rec P (Coeq_unrec f g h).1 (Coeq_unrec f g h).2 =
h
    apply path_arrow.
H: Funext
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
Coeq_rec P (Coeq_unrec f g h).1 (Coeq_unrec f g h).2 ==
h
    srapply Coeq_ind; intros b.
H: Funext
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
b: A
(fun w : Coeq f g =>
 Coeq_rec P (Coeq_unrec f g h).1 (Coeq_unrec f g h).2
   w = h w) (coeq b)
H: Funext
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
b: B
transport
  (fun w : Coeq f g =>
   Coeq_rec P (Coeq_unrec f g h).1
     (Coeq_unrec f g h).2 w = h w) (cglue b)
  ((fun b : A => ?Goal) (f b)) =
(fun b : A => ?Goal) (g b)
    1: cbn;reflexivity.
H: Funext
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
b: B
transport
  (fun w : Coeq f g =>
   Coeq_rec P (Coeq_unrec f g h).1
     (Coeq_unrec f g h).2 w = h w) (cglue b)
  ((fun b : A =>
    1
    :
    (fun w : Coeq f g =>
     Coeq_rec P (Coeq_unrec f g h).1
       (Coeq_unrec f g h).2 w = h w) (coeq b)) (f b)) =
(fun b : A =>
 1
 :
 (fun w : Coeq f g =>
  Coeq_rec P (Coeq_unrec f g h).1 (Coeq_unrec f g h).2
    w = h w) (coeq b)) (g b)
    cbn.
H: Funext
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
b: B
transport
  (fun w : Coeq f g =>
   Coeq_rec P (fun x : A => h (coeq x))
     (fun b : B => ap h (cglue b)) w = h w) (cglue b)
  1 = 1
    transport_paths FlFr.
H: Funext
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
b: B
ap
  (Coeq_rec P (fun x : A => h (coeq x))
     (fun b : B => ap h (cglue b))) (cglue b) @ 1 =
1 @ ap h (cglue b)
    apply equiv_p1_1q.
H: Funext
B, A: Type
f, g: B -> A
P: Type
h: Coeq f g -> P
b: B
ap
  (Coeq_rec P (fun x : A => h (coeq x))
     (fun b : B => ap h (cglue b))) (cglue b) =
ap h (cglue b)
    napply Coeq_rec_beta_cglue.
  -
H: Funext
B, A: Type
f, g: B -> A
P: Type
Coeq_unrec f g
o (fun p : {h : A -> P & h o f == h o g} =>
   Coeq_rec P p.1 p.2) == idmap intros [h q]; srapply path_sigma'.
H: Funext
B, A: Type
f, g: B -> A
P: Type
h: A -> P
q: (fun x : B => h (f x)) == (fun x : B => h (g x))
(fun x : A => Coeq_rec P (h; q).1 (h; q).2 (coeq x)) =
h
H: Funext
B, A: Type
f, g: B -> A
P: Type
h: A -> P
q: (fun x : B => h (f x)) == (fun x : B => h (g x))
transport
  (fun k : A -> P =>
   (fun x : B => k (f x)) == (fun x : B => k (g x)))
  ?p
  (fun b : B =>
   ap (Coeq_rec P (h; q).1 (h; q).2) (cglue b)) = q
    +
H: Funext
B, A: Type
f, g: B -> A
P: Type
h: A -> P
q: (fun x : B => h (f x)) == (fun x : B => h (g x))
(fun x : A => Coeq_rec P (h; q).1 (h; q).2 (coeq x)) =
h reflexivity.
    +
H: Funext
B, A: Type
f, g: B -> A
P: Type
h: A -> P
q: (fun x : B => h (f x)) == (fun x : B => h (g x))
transport
  (fun k : A -> P =>
   (fun x : B => k (f x)) == (fun x : B => k (g x))) 1
  (fun b : B =>
   ap (Coeq_rec P (h; q).1 (h; q).2) (cglue b)) = q cbn.
H: Funext
B, A: Type
f, g: B -> A
P: Type
h: A -> P
q: (fun x : B => h (f x)) == (fun x : B => h (g x))
(fun b : B => ap (Coeq_rec P h q) (cglue b)) = q
      rapply path_forall; intros b.
H: Funext
B, A: Type
f, g: B -> A
P: Type
h: A -> P
q: (fun x : B => h (f x)) == (fun x : B => h (g x))
b: B
ap (Coeq_rec P h q) (cglue b) = q b
      apply Coeq_rec_beta_cglue.
Defined.

Definition equiv_Coeq_rec `{Funext} {B A} (f g : B -> A) P
  : {h : A -> P & h o f == h o g} <~> (Coeq f g -> P)
  := Build_Equiv _ _ _ (isequiv_Coeq_rec f g P).

(** ** Functoriality *)

Definition functor_coeq {B A f g B' A' f' g'}
           (h : B -> B') (k : A -> A')
           (p : k o f == f' o h) (q : k o g == g' o h)
: @Coeq B A f g -> @Coeq B' A' f' g'.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
Coeq f g -> Coeq f' g'
Proof.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
Coeq f g -> Coeq f' g'
  refine (Coeq_rec _ (coeq o k) _); intros b.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
b: B
coeq (k (f b)) = coeq (k (g b))
  refine (ap coeq (p b) @ _ @ ap coeq (q b)^).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
b: B
coeq (f' (h b)) = coeq (g' (h b))
  apply cglue.
Defined.

Definition functor_coeq_beta_cglue {B A f g B' A' f' g'}
           (h : B -> B') (k : A -> A')
           (p : k o f == f' o h) (q : k o g == g' o h)
           (b : B)
: ap (functor_coeq h k p q) (cglue b)
  = ap coeq (p b) @ cglue (h b) @ ap coeq (q b)^
:= (Coeq_rec_beta_cglue _ _ _ b).

Definition functor_coeq_idmap {B A f g}
  : functor_coeq (B:=B) (A:=A) (f:=f) (g:=g) idmap idmap (fun _ => 1) (fun _  => 1)
    == idmap.
B, A: Type
f, g: B -> A
functor_coeq idmap idmap (fun x : B => 1)
  (fun x : B => 1) == idmap
Proof.
B, A: Type
f, g: B -> A
functor_coeq idmap idmap (fun x : B => 1)
  (fun x : B => 1) == idmap
  snapply Coeq_ind.
B, A: Type
f, g: B -> A
forall a : A,
(fun w : Coeq f g =>
 functor_coeq idmap idmap (fun x : B => 1)
   (fun x : B => 1) w = idmap w) (coeq a)
B, A: Type
f, g: B -> A
forall b : B,
transport
  (fun w : Coeq f g =>
   functor_coeq idmap idmap (fun x : B => 1)
     (fun x : B => 1) w = idmap w) (cglue b)
  (?coeq' (f b)) = ?coeq' (g b)
  1: reflexivity.
B, A: Type
f, g: B -> A
forall b : B,
transport
  (fun w : Coeq f g =>
   functor_coeq idmap idmap (fun x : B => 1)
     (fun x : B => 1) w = idmap w) (cglue b)
  ((fun a : A => 1) (f b)) = (fun a : A => 1) (g b)
  intros b.
B, A: Type
f, g: B -> A
b: B
transport
  (fun w : Coeq f g =>
   functor_coeq idmap idmap (fun x : B => 1)
     (fun x : B => 1) w = idmap w) (cglue b)
  ((fun a : A => 1) (f b)) = (fun a : A => 1) (g b)
  transport_paths Flr.
B, A: Type
f, g: B -> A
b: B
ap
  (functor_coeq idmap idmap (fun x : B => 1)
     (fun x : B => 1)) (cglue b) @ 1 = 1 @ cglue b
  apply moveR_pM.
B, A: Type
f, g: B -> A
b: B
ap
  (functor_coeq idmap idmap (fun x : B => 1)
     (fun x : B => 1)) (cglue b) = (1 @ cglue b) @ 1^
  napply functor_coeq_beta_cglue.
Defined.

Definition functor_coeq_compose {B A f g B' A' f' g' B'' A'' f'' g''}
           (h : B -> B') (k : A -> A')
           (p : k o f == f' o h) (q : k o g == g' o h)
           (h' : B' -> B'') (k' : A' -> A'')
           (p' : k' o f' == f'' o h') (q' : k' o g' == g'' o h')
: functor_coeq (h' o h) (k' o k)
               (fun b => ap k' (p b) @ p' (h b))
               (fun b => ap k' (q b) @ q' (h b))
  == functor_coeq h' k' p' q' o functor_coeq h k p q.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
B'', A'': Type
f'', g'': B'' -> A''
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B''
k': A' -> A''
p': k' o f' == f'' o h'
q': k' o g' == g'' o h'
functor_coeq (h' o h) (k' o k)
  (fun b : B => ap k' (p b) @ p' (h b))
  (fun b : B => ap k' (q b) @ q' (h b)) ==
functor_coeq h' k' p' q' o functor_coeq h k p q
Proof.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
B'', A'': Type
f'', g'': B'' -> A''
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B''
k': A' -> A''
p': k' o f' == f'' o h'
q': k' o g' == g'' o h'
functor_coeq (h' o h) (k' o k)
  (fun b : B => ap k' (p b) @ p' (h b))
  (fun b : B => ap k' (q b) @ q' (h b)) ==
functor_coeq h' k' p' q' o functor_coeq h k p q
  refine (Coeq_ind _ (fun a => 1) _); cbn; intros b.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
B'', A'': Type
f'', g'': B'' -> A''
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B''
k': A' -> A''
p': k' o f' == f'' o h'
q': k' o g' == g'' o h'
b: B
transport
  (fun w : Coeq f g =>
   functor_coeq (fun x : B => h' (h x))
     (fun x : A => k' (k x))
     (fun b : B => ap k' (p b) @ p' (h b))
     (fun b : B => ap k' (q b) @ q' (h b)) w =
   functor_coeq h' k' p' q' (functor_coeq h k p q w))
  (cglue b) 1 = 1
  transport_paths FlFr.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
B'', A'': Type
f'', g'': B'' -> A''
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B''
k': A' -> A''
p': k' o f' == f'' o h'
q': k' o g' == g'' o h'
b: B
ap
  (functor_coeq (fun x : B => h' (h x))
     (fun x : A => k' (k x))
     (fun b : B => ap k' (p b) @ p' (h b))
     (fun b : B => ap k' (q b) @ q' (h b))) (cglue b) @
1 =
1 @
ap
  (fun x : Coeq f g =>
   functor_coeq h' k' p' q' (functor_coeq h k p q x))
  (cglue b)
  apply equiv_p1_1q; symmetry.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
B'', A'': Type
f'', g'': B'' -> A''
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B''
k': A' -> A''
p': k' o f' == f'' o h'
q': k' o g' == g'' o h'
b: B
ap
  (fun x : Coeq f g =>
   functor_coeq h' k' p' q' (functor_coeq h k p q x))
  (cglue b) =
ap
  (functor_coeq (fun x : B => h' (h x))
     (fun x : A => k' (k x))
     (fun b : B => ap k' (p b) @ p' (h b))
     (fun b : B => ap k' (q b) @ q' (h b))) (cglue b)
  rewrite ap_compose.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
B'', A'': Type
f'', g'': B'' -> A''
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B''
k': A' -> A''
p': k' o f' == f'' o h'
q': k' o g' == g'' o h'
b: B
ap (functor_coeq h' k' p' q')
  (ap (functor_coeq h k p q) (cglue b)) =
ap
  (functor_coeq (fun x : B => h' (h x))
     (fun x : A => k' (k x))
     (fun b : B => ap k' (p b) @ p' (h b))
     (fun b : B => ap k' (q b) @ q' (h b))) (cglue b)
  rewrite !functor_coeq_beta_cglue, !ap_pp, functor_coeq_beta_cglue.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
B'', A'': Type
f'', g'': B'' -> A''
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B''
k': A' -> A''
p': k' o f' == f'' o h'
q': k' o g' == g'' o h'
b: B
(ap (functor_coeq h' k' p' q') (ap coeq (p b)) @
 ((ap coeq (p' (h b)) @ cglue (h' (h b))) @
  ap coeq (q' (h b))^)) @
ap (functor_coeq h' k' p' q') (ap coeq (q b)^) =
((ap coeq (ap k' (p b)) @ ap coeq (p' (h b))) @
 cglue (h' (h b))) @ ap coeq (ap k' (q b) @ q' (h b))^
  rewrite <- !ap_compose.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
B'', A'': Type
f'', g'': B'' -> A''
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B''
k': A' -> A''
p': k' o f' == f'' o h'
q': k' o g' == g'' o h'
b: B
(ap (fun x : A' => functor_coeq h' k' p' q' (coeq x))
   (p b) @
 ((ap coeq (p' (h b)) @ cglue (h' (h b))) @
  ap coeq (q' (h b))^)) @
ap (fun x : A' => functor_coeq h' k' p' q' (coeq x))
  (q b)^ =
((ap (fun x : A' => coeq (k' x)) (p b) @
  ap coeq (p' (h b))) @ cglue (h' (h b))) @
ap coeq (ap k' (q b) @ q' (h b))^ cbn.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
B'', A'': Type
f'', g'': B'' -> A''
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B''
k': A' -> A''
p': k' o f' == f'' o h'
q': k' o g' == g'' o h'
b: B
(ap (fun x : A' => functor_coeq h' k' p' q' (coeq x))
   (p b) @
 ((ap coeq (p' (h b)) @ cglue (h' (h b))) @
  ap coeq (q' (h b))^)) @
ap (fun x : A' => functor_coeq h' k' p' q' (coeq x))
  (q b)^ =
((ap (fun x : A' => coeq (k' x)) (p b) @
  ap coeq (p' (h b))) @ cglue (h' (h b))) @
ap coeq (ap k' (q b) @ q' (h b))^
  rewrite !ap_V, ap_pp, inv_pp, <- ap_compose, !concat_p_pp.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
B'', A'': Type
f'', g'': B'' -> A''
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B''
k': A' -> A''
p': k' o f' == f'' o h'
q': k' o g' == g'' o h'
b: B
(((ap
     (fun x : A' => functor_coeq h' k' p' q' (coeq x))
     (p b) @ ap coeq (p' (h b))) @ cglue (h' (h b))) @
 (ap coeq (q' (h b)))^) @
(ap (fun x : A' => functor_coeq h' k' p' q' (coeq x))
   (q b))^ =
(((ap (fun x : A' => coeq (k' x)) (p b) @
   ap coeq (p' (h b))) @ cglue (h' (h b))) @
 (ap coeq (q' (h b)))^) @
(ap (fun x : A' => coeq (k' x)) (q b))^
  reflexivity.
Qed.

Definition functor_coeq_homotopy {B A f g B' A' f' g'}
           (h : B -> B') (k : A -> A')
           (p : k o f == f' o h) (q : k o g == g' o h)
           (h' : B -> B') (k' : A -> A')
           (p' : k' o f == f' o h') (q' : k' o g == g' o h')
           (r : h == h') (s : k == k')
           (u : forall b, s (f b) @ p' b = p b @ ap f' (r b))
           (v : forall b, s (g b) @ q' b = q b @ ap g' (r b))
: functor_coeq h k p q == functor_coeq h' k' p' q'.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B -> B'
k': A -> A'
p': k' o f == f' o h'
q': k' o g == g' o h'
r: h == h'
s: k == k'
u: forall b : B, s (f b) @ p' b = p b @ ap f' (r b)
v: forall b : B, s (g b) @ q' b = q b @ ap g' (r b)
functor_coeq h k p q == functor_coeq h' k' p' q'
Proof.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B -> B'
k': A -> A'
p': k' o f == f' o h'
q': k' o g == g' o h'
r: h == h'
s: k == k'
u: forall b : B, s (f b) @ p' b = p b @ ap f' (r b)
v: forall b : B, s (g b) @ q' b = q b @ ap g' (r b)
functor_coeq h k p q == functor_coeq h' k' p' q'
  refine (Coeq_ind _ (fun a => ap coeq (s a)) _); cbn; intros b.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B -> B'
k': A -> A'
p': k' o f == f' o h'
q': k' o g == g' o h'
r: h == h'
s: k == k'
u: forall b : B, s (f b) @ p' b = p b @ ap f' (r b)
v: forall b : B, s (g b) @ q' b = q b @ ap g' (r b)
b: B
transport
  (fun w : Coeq f g =>
   functor_coeq h k p q w = functor_coeq h' k' p' q' w)
  (cglue b) (ap coeq (s (f b))) = ap coeq (s (g b))
  transport_paths FlFr.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B -> B'
k': A -> A'
p': k' o f == f' o h'
q': k' o g == g' o h'
r: h == h'
s: k == k'
u: forall b : B, s (f b) @ p' b = p b @ ap f' (r b)
v: forall b : B, s (g b) @ q' b = q b @ ap g' (r b)
b: B
ap (functor_coeq h k p q) (cglue b) @
ap coeq (s (g b)) =
ap coeq (s (f b)) @
ap (functor_coeq h' k' p' q') (cglue b)
  rewrite !functor_coeq_beta_cglue.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B -> B'
k': A -> A'
p': k' o f == f' o h'
q': k' o g == g' o h'
r: h == h'
s: k == k'
u: forall b : B, s (f b) @ p' b = p b @ ap f' (r b)
v: forall b : B, s (g b) @ q' b = q b @ ap g' (r b)
b: B
((ap coeq (p b) @ cglue (h b)) @ ap coeq (q b)^) @
ap coeq (s (g b)) =
ap coeq (s (f b)) @
((ap coeq (p' b) @ cglue (h' b)) @ ap coeq (q' b)^)
  Open Scope long_path_scope.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B -> B'
k': A -> A'
p': k' o f == f' o h'
q': k' o g == g' o h'
r: h == h'
s: k == k'
u: forall b : B, s (f b)
              @' p' b = p b
                        @' ap f' (r b)
v: forall b : B, s (g b)
              @' q' b = q b
                        @' ap g' (r b)
b: B
ap coeq (p b)
@' cglue (h b)
@' ap coeq (q b)^
@' ap coeq (s (g b)) =
ap coeq (s (f b))
@' (ap coeq (p' b)
    @' cglue (h' b)
    @' ap coeq (q' b)^)
  rewrite 2 ap_V.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B -> B'
k': A -> A'
p': k' o f == f' o h'
q': k' o g == g' o h'
r: h == h'
s: k == k'
u: forall b : B, s (f b)
              @' p' b = p b
                        @' ap f' (r b)
v: forall b : B, s (g b)
              @' q' b = q b
                        @' ap g' (r b)
b: B
ap coeq (p b)
@' cglue (h b)
@' (ap coeq (q b))^
@' ap coeq (s (g b)) =
ap coeq (s (f b))
@' (ap coeq (p' b)
    @' cglue (h' b)
    @' (ap coeq (q' b))^)
  rewrite !concat_p_pp.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B -> B'
k': A -> A'
p': k' o f == f' o h'
q': k' o g == g' o h'
r: h == h'
s: k == k'
u: forall b : B, s (f b)
              @' p' b = p b
                        @' ap f' (r b)
v: forall b : B, s (g b)
              @' q' b = q b
                        @' ap g' (r b)
b: B
ap coeq (p b)
@' cglue (h b)
@' (ap coeq (q b))^
@' ap coeq (s (g b)) =
ap coeq (s (f b))
@' ap coeq (p' b)
@' cglue (h' b)
@' (ap coeq (q' b))^
  apply moveL_pV.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B -> B'
k': A -> A'
p': k' o f == f' o h'
q': k' o g == g' o h'
r: h == h'
s: k == k'
u: forall b : B, s (f b)
              @' p' b = p b
                        @' ap f' (r b)
v: forall b : B, s (g b)
              @' q' b = q b
                        @' ap g' (r b)
b: B
ap coeq (p b)
@' cglue (h b)
@' (ap coeq (q b))^
@' ap coeq (s (g b))
@' ap coeq (q' b) =
ap coeq (s (f b))
@' ap coeq (p' b)
@' cglue (h' b)
  rewrite <- (ap_pp (@coeq _ _ f' g') (s (f b)) (p' b)).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B -> B'
k': A -> A'
p': k' o f == f' o h'
q': k' o g == g' o h'
r: h == h'
s: k == k'
u: forall b : B, s (f b)
              @' p' b = p b
                        @' ap f' (r b)
v: forall b : B, s (g b)
              @' q' b = q b
                        @' ap g' (r b)
b: B
ap coeq (p b)
@' cglue (h b)
@' (ap coeq (q b))^
@' ap coeq (s (g b))
@' ap coeq (q' b) =
ap coeq (s (f b)
         @' p' b)
@' cglue (h' b)
  rewrite u, ap_pp.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B -> B'
k': A -> A'
p': k' o f == f' o h'
q': k' o g == g' o h'
r: h == h'
s: k == k'
u: forall b : B, s (f b)
              @' p' b = p b
                        @' ap f' (r b)
v: forall b : B, s (g b)
              @' q' b = q b
                        @' ap g' (r b)
b: B
ap coeq (p b)
@' cglue (h b)
@' (ap coeq (q b))^
@' ap coeq (s (g b))
@' ap coeq (q' b) =
ap coeq (p b)
@' ap coeq (ap f' (r b))
@' cglue (h' b)
  rewrite !concat_pp_p; apply whiskerL.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B -> B'
k': A -> A'
p': k' o f == f' o h'
q': k' o g == g' o h'
r: h == h'
s: k == k'
u: forall b : B, s (f b)
              @' p' b = p b
                        @' ap f' (r b)
v: forall b : B, s (g b)
              @' q' b = q b
                        @' ap g' (r b)
b: B
cglue (h b)
@' ((ap coeq (q b))^
    @' (ap coeq (s (g b))
        @' ap coeq (q' b))) =
ap coeq (ap f' (r b))
@' cglue (h' b)
  rewrite <- (ap_pp (@coeq _ _ f' g') (s (g b)) (q' b)).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B -> B'
k': A -> A'
p': k' o f == f' o h'
q': k' o g == g' o h'
r: h == h'
s: k == k'
u: forall b : B, s (f b)
              @' p' b = p b
                        @' ap f' (r b)
v: forall b : B, s (g b)
              @' q' b = q b
                        @' ap g' (r b)
b: B
cglue (h b)
@' ((ap coeq (q b))^
    @' ap coeq (s (g b)
                @' q' b)) =
ap coeq (ap f' (r b))
@' cglue (h' b)
  rewrite v, ap_pp.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B -> B'
k': A -> A'
p': k' o f == f' o h'
q': k' o g == g' o h'
r: h == h'
s: k == k'
u: forall b : B, s (f b)
              @' p' b = p b
                        @' ap f' (r b)
v: forall b : B, s (g b)
              @' q' b = q b
                        @' ap g' (r b)
b: B
cglue (h b)
@' ((ap coeq (q b))^
    @' (ap coeq (q b)
        @' ap coeq (ap g' (r b)))) =
ap coeq (ap f' (r b))
@' cglue (h' b)
  rewrite concat_V_pp.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B -> B'
k': A -> A'
p': k' o f == f' o h'
q': k' o g == g' o h'
r: h == h'
s: k == k'
u: forall b : B, s (f b)
              @' p' b = p b
                        @' ap f' (r b)
v: forall b : B, s (g b)
              @' q' b = q b
                        @' ap g' (r b)
b: B
cglue (h b)
@' ap coeq (ap g' (r b)) =
ap coeq (ap f' (r b))
@' cglue (h' b)
  rewrite <- 2 ap_compose.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B -> B'
k': A -> A'
p': k' o f == f' o h'
q': k' o g == g' o h'
r: h == h'
s: k == k'
u: forall b : B, s (f b)
              @' p' b = p b
                        @' ap f' (r b)
v: forall b : B, s (g b)
              @' q' b = q b
                        @' ap g' (r b)
b: B
cglue (h b)
@' ap (fun x : B' => coeq (g' x)) (r b) =
ap (fun x : B' => coeq (f' x)) (r b)
@' cglue (h' b)
  exact (concat_Ap (@cglue _ _ f' g') (r b))^.
  Close Scope long_path_scope.
Qed.

Definition functor_coeq_sect {B A f g B' A' f' g'}
           (h : B -> B') (k : A -> A')
           (p : k o f == f' o h) (q : k o g == g' o h)
           (h' : B' -> B) (k' : A' -> A)
           (p' : k' o f' == f o h') (q' : k' o g' == g o h')
           (r : h' o h == idmap) (s : k' o k == idmap)
           (u : forall b, ap k' (p b) @ p' (h b) @ ap f (r b) = s (f b))
           (v : forall b, ap k' (q b) @ q' (h b) @ ap g (r b) = s (g b))
: (functor_coeq h' k' p' q') o (functor_coeq h k p q) == idmap.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B
k': A' -> A
p': k' o f' == f o h'
q': k' o g' == g o h'
r: h' o h == idmap
s: k' o k == idmap
u: forall b : B,
(ap k' (p b) @ p' (h b)) @ ap f (r b) = s (f b)
v: forall b : B,
(ap k' (q b) @ q' (h b)) @ ap g (r b) = s (g b)
functor_coeq h' k' p' q' o functor_coeq h k p q ==
idmap
Proof.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B
k': A' -> A
p': k' o f' == f o h'
q': k' o g' == g o h'
r: h' o h == idmap
s: k' o k == idmap
u: forall b : B,
(ap k' (p b) @ p' (h b)) @ ap f (r b) = s (f b)
v: forall b : B,
(ap k' (q b) @ q' (h b)) @ ap g (r b) = s (g b)
functor_coeq h' k' p' q' o functor_coeq h k p q ==
idmap
  refine (Coeq_ind _ (fun a => ap coeq (s a)) _); cbn; intros b.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B
k': A' -> A
p': k' o f' == f o h'
q': k' o g' == g o h'
r: h' o h == idmap
s: k' o k == idmap
u: forall b : B,
(ap k' (p b) @ p' (h b)) @ ap f (r b) = s (f b)
v: forall b : B,
(ap k' (q b) @ q' (h b)) @ ap g (r b) = s (g b)
b: B
transport
  (fun w : Coeq f g =>
   functor_coeq h' k' p' q' (functor_coeq h k p q w) =
   w) (cglue b) (ap coeq (s (f b))) =
ap coeq (s (g b))
  refine (transport_paths_FFlr (cglue b) _ @ _).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B
k': A' -> A
p': k' o f' == f o h'
q': k' o g' == g o h'
r: h' o h == idmap
s: k' o k == idmap
u: forall b : B,
(ap k' (p b) @ p' (h b)) @ ap f (r b) = s (f b)
v: forall b : B,
(ap k' (q b) @ q' (h b)) @ ap g (r b) = s (g b)
b: B
((ap (functor_coeq h' k' p' q')
    (ap (functor_coeq h k p q) (cglue b)))^ @
 ap coeq (s (f b))) @ cglue b = ap coeq (s (g b))
  rewrite concat_pp_p; apply moveR_Vp.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B
k': A' -> A
p': k' o f' == f o h'
q': k' o g' == g o h'
r: h' o h == idmap
s: k' o k == idmap
u: forall b : B,
(ap k' (p b) @ p' (h b)) @ ap f (r b) = s (f b)
v: forall b : B,
(ap k' (q b) @ q' (h b)) @ ap g (r b) = s (g b)
b: B
ap coeq (s (f b)) @ cglue b =
ap (functor_coeq h' k' p' q')
  (ap (functor_coeq h k p q) (cglue b)) @
ap coeq (s (g b))
  rewrite functor_coeq_beta_cglue, !ap_pp.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B
k': A' -> A
p': k' o f' == f o h'
q': k' o g' == g o h'
r: h' o h == idmap
s: k' o k == idmap
u: forall b : B,
(ap k' (p b) @ p' (h b)) @ ap f (r b) = s (f b)
v: forall b : B,
(ap k' (q b) @ q' (h b)) @ ap g (r b) = s (g b)
b: B
ap coeq (s (f b)) @ cglue b =
((ap (functor_coeq h' k' p' q') (ap coeq (p b)) @
  ap (functor_coeq h' k' p' q') (cglue (h b))) @
 ap (functor_coeq h' k' p' q') (ap coeq (q b)^)) @
ap coeq (s (g b))
  rewrite <- !ap_compose; cbn.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B
k': A' -> A
p': k' o f' == f o h'
q': k' o g' == g o h'
r: h' o h == idmap
s: k' o k == idmap
u: forall b : B,
(ap k' (p b) @ p' (h b)) @ ap f (r b) = s (f b)
v: forall b : B,
(ap k' (q b) @ q' (h b)) @ ap g (r b) = s (g b)
b: B
ap coeq (s (f b)) @ cglue b =
((ap (fun x : A' => functor_coeq h' k' p' q' (coeq x))
    (p b) @
  ap (functor_coeq h' k' p' q') (cglue (h b))) @
 ap (fun x : A' => functor_coeq h' k' p' q' (coeq x))
   (q b)^) @ ap coeq (s (g b))
  rewrite functor_coeq_beta_cglue.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B
k': A' -> A
p': k' o f' == f o h'
q': k' o g' == g o h'
r: h' o h == idmap
s: k' o k == idmap
u: forall b : B,
(ap k' (p b) @ p' (h b)) @ ap f (r b) = s (f b)
v: forall b : B,
(ap k' (q b) @ q' (h b)) @ ap g (r b) = s (g b)
b: B
ap coeq (s (f b)) @ cglue b =
((ap (fun x : A' => functor_coeq h' k' p' q' (coeq x))
    (p b) @
  ((ap coeq (p' (h b)) @ cglue (h' (h b))) @
   ap coeq (q' (h b))^)) @
 ap (fun x : A' => functor_coeq h' k' p' q' (coeq x))
   (q b)^) @ ap coeq (s (g b))
  Open Scope long_path_scope.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B
k': A' -> A
p': k' o f' == f o h'
q': k' o g' == g o h'
r: h' o h == idmap
s: k' o k == idmap
u: forall b : B,
ap k' (p b)
@' p' (h b)
@' ap f (r b) = s (f b)
v: forall b : B,
ap k' (q b)
@' q' (h b)
@' ap g (r b) = s (g b)
b: B
ap coeq (s (f b))
@' cglue b =
ap (fun x : A' => functor_coeq h' k' p' q' (coeq x))
  (p b)
@' (ap coeq (p' (h b))
    @' cglue (h' (h b))
    @' ap coeq (q' (h b))^)
@' ap
     (fun x : A' => functor_coeq h' k' p' q' (coeq x))
     (q b)^
@' ap coeq (s (g b))
  rewrite !concat_p_pp.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B
k': A' -> A
p': k' o f' == f o h'
q': k' o g' == g o h'
r: h' o h == idmap
s: k' o k == idmap
u: forall b : B,
ap k' (p b)
@' p' (h b)
@' ap f (r b) = s (f b)
v: forall b : B,
ap k' (q b)
@' q' (h b)
@' ap g (r b) = s (g b)
b: B
ap coeq (s (f b))
@' cglue b =
ap (fun x : A' => functor_coeq h' k' p' q' (coeq x))
  (p b)
@' ap coeq (p' (h b))
@' cglue (h' (h b))
@' ap coeq (q' (h b))^
@' ap
     (fun x : A' => functor_coeq h' k' p' q' (coeq x))
     (q b)^
@' ap coeq (s (g b))
  rewrite <- u, !ap_pp, !(ap_compose k' coeq).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B
k': A' -> A
p': k' o f' == f o h'
q': k' o g' == g o h'
r: h' o h == idmap
s: k' o k == idmap
u: forall b : B,
ap k' (p b)
@' p' (h b)
@' ap f (r b) = s (f b)
v: forall b : B,
ap k' (q b)
@' q' (h b)
@' ap g (r b) = s (g b)
b: B
ap coeq (ap k' (p b))
@' ap coeq (p' (h b))
@' ap coeq (ap f (r b))
@' cglue b =
ap coeq (ap k' (p b))
@' ap coeq (p' (h b))
@' cglue (h' (h b))
@' ap coeq (q' (h b))^
@' ap coeq (ap k' (q b)^)
@' ap coeq (s (g b))
  rewrite !concat_pp_p; do 2 apply whiskerL.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B
k': A' -> A
p': k' o f' == f o h'
q': k' o g' == g o h'
r: h' o h == idmap
s: k' o k == idmap
u: forall b : B,
ap k' (p b)
@' p' (h b)
@' ap f (r b) = s (f b)
v: forall b : B,
ap k' (q b)
@' q' (h b)
@' ap g (r b) = s (g b)
b: B
ap coeq (ap f (r b))
@' cglue b =
cglue (h' (h b))
@' (ap coeq (q' (h b))^
    @' (ap coeq (ap k' (q b)^)
        @' ap coeq (s (g b))))
  rewrite !concat_p_pp.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B
k': A' -> A
p': k' o f' == f o h'
q': k' o g' == g o h'
r: h' o h == idmap
s: k' o k == idmap
u: forall b : B,
ap k' (p b)
@' p' (h b)
@' ap f (r b) = s (f b)
v: forall b : B,
ap k' (q b)
@' q' (h b)
@' ap g (r b) = s (g b)
b: B
ap coeq (ap f (r b))
@' cglue b =
cglue (h' (h b))
@' ap coeq (q' (h b))^
@' ap coeq (ap k' (q b)^)
@' ap coeq (s (g b))
  rewrite <- v.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B
k': A' -> A
p': k' o f' == f o h'
q': k' o g' == g o h'
r: h' o h == idmap
s: k' o k == idmap
u: forall b : B,
ap k' (p b)
@' p' (h b)
@' ap f (r b) = s (f b)
v: forall b : B,
ap k' (q b)
@' q' (h b)
@' ap g (r b) = s (g b)
b: B
ap coeq (ap f (r b))
@' cglue b =
cglue (h' (h b))
@' ap coeq (q' (h b))^
@' ap coeq (ap k' (q b)^)
@' ap coeq (ap k' (q b)
            @' q' (h b)
            @' ap g (r b))
  rewrite !ap_pp, !ap_V, !concat_p_pp, !concat_pV_p.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B
k': A' -> A
p': k' o f' == f o h'
q': k' o g' == g o h'
r: h' o h == idmap
s: k' o k == idmap
u: forall b : B,
ap k' (p b)
@' p' (h b)
@' ap f (r b) = s (f b)
v: forall b : B,
ap k' (q b)
@' q' (h b)
@' ap g (r b) = s (g b)
b: B
ap coeq (ap f (r b))
@' cglue b = cglue (h' (h b))
             @' ap coeq (ap g (r b))
  rewrite <- !ap_compose.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
h': B' -> B
k': A' -> A
p': k' o f' == f o h'
q': k' o g' == g o h'
r: h' o h == idmap
s: k' o k == idmap
u: forall b : B,
ap k' (p b)
@' p' (h b)
@' ap f (r b) = s (f b)
v: forall b : B,
ap k' (q b)
@' q' (h b)
@' ap g (r b) = s (g b)
b: B
ap (fun x : B => coeq (f x)) (r b)
@' cglue b =
cglue (h' (h b))
@' ap (fun x : B => coeq (g x)) (r b)
  exact (concat_Ap cglue (r b)).
  Close Scope long_path_scope.
Qed.

Section IsEquivFunctorCoeq.

  Context {B A f g B' A' f' g'}
          (h : B -> B') (k : A -> A')
          `{IsEquiv _ _ h} `{IsEquiv _ _ k}
          (p : k o f == f' o h) (q : k o g == g' o h).

  Definition functor_coeq_inverse
  : @Coeq B' A' f' g' -> @Coeq B A f g.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
Coeq f' g' -> Coeq f g
  Proof.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
Coeq f' g' -> Coeq f g
    refine (functor_coeq h^-1 k^-1 _ _).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
(fun x : B' => k^-1 (f' x)) ==
(fun x : B' => f (h^-1 x))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
(fun x : B' => k^-1 (g' x)) ==
(fun x : B' => g (h^-1 x))
    -
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
(fun x : B' => k^-1 (f' x)) ==
(fun x : B' => f (h^-1 x)) intros b.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
k^-1 (f' b) = f (h^-1 b)
      refine (ap (k^-1 o f') (eisretr h b)^ @ _ @ eissect k (f (h^-1 b))).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
k^-1 (f' (h (h^-1 b))) = k^-1 (k (f (h^-1 b)))
      apply ap, inverse, p.
    -
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
(fun x : B' => k^-1 (g' x)) ==
(fun x : B' => g (h^-1 x)) intros b.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
k^-1 (g' b) = g (h^-1 b)
      refine (ap (k^-1 o g') (eisretr h b)^ @ _ @ eissect k (g (h^-1 b))).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
k^-1 (g' (h (h^-1 b))) = k^-1 (k (g (h^-1 b)))
      apply ap, inverse, q.
  Defined.

  Definition functor_coeq_eissect
  : (functor_coeq h k p q) o functor_coeq_inverse == idmap.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
functor_coeq h k p q o functor_coeq_inverse == idmap
  Proof.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
functor_coeq h k p q o functor_coeq_inverse == idmap
    Open Scope long_path_scope.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
functor_coeq h k p q o functor_coeq_inverse == idmap
    refine (functor_coeq_sect _ _ _ _ _ _ _ _
                              (eisretr h) (eisretr k) _ _); intros b.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
ap k
  (ap (fun x : B' => k^-1 (f' x)) (eisretr h b)^
   @' ap k^-1 (p (h^-1 b))^
   @' eissect k (f (h^-1 b)))
@' p (h^-1 b)
@' ap f' (eisretr h b) = eisretr k (f' b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
ap k
  (ap (fun x : B' => k^-1 (g' x)) (eisretr h b)^
   @' ap k^-1 (q (h^-1 b))^
   @' eissect k (g (h^-1 b)))
@' q (h^-1 b)
@' ap g' (eisretr h b) = eisretr k (g' b)
    (** The two proofs are identical modulo replacing [f] by [g], [f'] by [g'], and [p] by [q]. *)
    all:rewrite !ap_pp, <- eisadj.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
ap k (ap (fun x : B' => k^-1 (f' x)) (eisretr h b)^)
@' ap k (ap k^-1 (p (h^-1 b))^)
@' eisretr k (k (f (h^-1 b)))
@' p (h^-1 b)
@' ap f' (eisretr h b) = eisretr k (f' b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
ap k (ap (fun x : B' => k^-1 (g' x)) (eisretr h b)^)
@' ap k (ap k^-1 (q (h^-1 b))^)
@' eisretr k (k (g (h^-1 b)))
@' q (h^-1 b)
@' ap g' (eisretr h b) = eisretr k (g' b)
    all:rewrite <- !ap_compose.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
ap k (ap (fun x : B' => k^-1 (f' x)) (eisretr h b)^)
@' ap (fun x : A' => k (k^-1 x)) (p (h^-1 b))^
@' eisretr k (k (f (h^-1 b)))
@' p (h^-1 b)
@' ap f' (eisretr h b) = eisretr k (f' b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
ap k (ap (fun x : B' => k^-1 (g' x)) (eisretr h b)^)
@' ap (fun x : A' => k (k^-1 x)) (q (h^-1 b))^
@' eisretr k (k (g (h^-1 b)))
@' q (h^-1 b)
@' ap g' (eisretr h b) = eisretr k (g' b)
    all:rewrite (concat_pA1_p (eisretr k) _ _).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
ap k (ap (fun x : B' => k^-1 (f' x)) (eisretr h b)^)
@' eisretr k (f' (h (h^-1 b)))
@' (p (h^-1 b))^
@' p (h^-1 b)
@' ap f' (eisretr h b) = eisretr k (f' b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
ap k (ap (fun x : B' => k^-1 (g' x)) (eisretr h b)^)
@' eisretr k (g' (h (h^-1 b)))
@' (q (h^-1 b))^
@' q (h^-1 b)
@' ap g' (eisretr h b) = eisretr k (g' b)
    all:rewrite concat_pV_p.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
ap k (ap (fun x : B' => k^-1 (f' x)) (eisretr h b)^)
@' eisretr k (f' (h (h^-1 b)))
@' ap f' (eisretr h b) = eisretr k (f' b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
ap k (ap (fun x : B' => k^-1 (g' x)) (eisretr h b)^)
@' eisretr k (g' (h (h^-1 b)))
@' ap g' (eisretr h b) = eisretr k (g' b)
    all:rewrite <- (ap_compose (k^-1 o _) k).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
ap (fun x : B' => k (k^-1 (f' x))) (eisretr h b)^
@' eisretr k (f' (h (h^-1 b)))
@' ap f' (eisretr h b) = eisretr k (f' b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
ap (fun x : B' => k (k^-1 (g' x))) (eisretr h b)^
@' eisretr k (g' (h (h^-1 b)))
@' ap g' (eisretr h b) = eisretr k (g' b)
    all:rewrite (ap_compose _ (k o k^-1)).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
ap (fun x : A' => k (k^-1 x)) (ap f' (eisretr h b)^)
@' eisretr k (f' (h (h^-1 b)))
@' ap f' (eisretr h b) = eisretr k (f' b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
ap (fun x : A' => k (k^-1 x)) (ap g' (eisretr h b)^)
@' eisretr k (g' (h (h^-1 b)))
@' ap g' (eisretr h b) = eisretr k (g' b)
    all:rewrite (concat_A1p (eisretr k) (ap _ (eisretr h b)^)).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
eisretr k (f' b)
@' ap f' (eisretr h b)^
@' ap f' (eisretr h b) = eisretr k (f' b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B'
eisretr k (g' b)
@' ap g' (eisretr h b)^
@' ap g' (eisretr h b) = eisretr k (g' b)
    all:rewrite ap_V, concat_pV_p; reflexivity.
    Close Scope long_path_scope.
  Qed.

  Definition functor_coeq_eisretr
  : functor_coeq_inverse o (functor_coeq h k p q) == idmap.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
functor_coeq_inverse o functor_coeq h k p q == idmap
  Proof.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
functor_coeq_inverse o functor_coeq h k p q == idmap
    Open Scope long_path_scope.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
functor_coeq_inverse o functor_coeq h k p q == idmap
    refine (functor_coeq_sect _ _ _ _ _ _ _ _
                              (eissect h) (eissect k) _ _); intros b.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
ap k^-1 (p b)
@' (ap (fun x : B' => k^-1 (f' x)) (eisretr h (h b))^
    @' ap k^-1 (p (h^-1 (h b)))^
    @' eissect k (f (h^-1 (h b))))
@' ap f (eissect h b) = eissect k (f b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
ap k^-1 (q b)
@' (ap (fun x : B' => k^-1 (g' x)) (eisretr h (h b))^
    @' ap k^-1 (q (h^-1 (h b)))^
    @' eissect k (g (h^-1 (h b))))
@' ap g (eissect h b) = eissect k (g b)
    all:rewrite !concat_p_pp, eisadj, <- ap_V, <- !ap_compose.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
ap k^-1 (p b)
@' ap (fun x : B => k^-1 (f' (h x))) (eissect h b)^
@' ap k^-1 (p (h^-1 (h b)))^
@' eissect k (f (h^-1 (h b)))
@' ap f (eissect h b) = eissect k (f b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
ap k^-1 (q b)
@' ap (fun x : B => k^-1 (g' (h x))) (eissect h b)^
@' ap k^-1 (q (h^-1 (h b)))^
@' eissect k (g (h^-1 (h b)))
@' ap g (eissect h b) = eissect k (g b)
    all:rewrite (ap_compose (_ o h) k^-1).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
ap k^-1 (p b)
@' ap k^-1 (ap (fun x : B => f' (h x)) (eissect h b)^)
@' ap k^-1 (p (h^-1 (h b)))^
@' eissect k (f (h^-1 (h b)))
@' ap f (eissect h b) = eissect k (f b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
ap k^-1 (q b)
@' ap k^-1 (ap (fun x : B => g' (h x)) (eissect h b)^)
@' ap k^-1 (q (h^-1 (h b)))^
@' eissect k (g (h^-1 (h b)))
@' ap g (eissect h b) = eissect k (g b)
    all:rewrite <- !(ap_pp k^-1), !concat_pp_p.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
ap k^-1
  (p b
   @' (ap (fun x : B => f' (h x)) (eissect h b)^
       @' (p (h^-1 (h b)))^))
@' (eissect k (f (h^-1 (h b)))
    @' ap f (eissect h b)) = eissect k (f b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
ap k^-1
  (q b
   @' (ap (fun x : B => g' (h x)) (eissect h b)^
       @' (q (h^-1 (h b)))^))
@' (eissect k (g (h^-1 (h b)))
    @' ap g (eissect h b)) = eissect k (g b)
    1:rewrite (concat_Ap (fun b => (p b)^) (eissect h b)^).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
ap k^-1
  (p b
   @' ((p b)^
       @' ap (fun b : B => k (f b)) (eissect h b)^))
@' (eissect k (f (h^-1 (h b)))
    @' ap f (eissect h b)) = eissect k (f b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
ap k^-1
  (q b
   @' (ap (fun x : B => g' (h x)) (eissect h b)^
       @' (q (h^-1 (h b)))^))
@' (eissect k (g (h^-1 (h b)))
    @' ap g (eissect h b)) = eissect k (g b)
    2:rewrite (concat_Ap (fun b => (q b)^) (eissect h b)^).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
ap k^-1
  (p b
   @' ((p b)^
       @' ap (fun b : B => k (f b)) (eissect h b)^))
@' (eissect k (f (h^-1 (h b)))
    @' ap f (eissect h b)) = eissect k (f b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
ap k^-1
  (q b
   @' ((q b)^
       @' ap (fun b : B => k (g b)) (eissect h b)^))
@' (eissect k (g (h^-1 (h b)))
    @' ap g (eissect h b)) = eissect k (g b)
    all:rewrite concat_p_Vp, concat_p_pp.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
ap k^-1 (ap (fun b : B => k (f b)) (eissect h b)^)
@' eissect k (f (h^-1 (h b)))
@' ap f (eissect h b) = eissect k (f b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
ap k^-1 (ap (fun b : B => k (g b)) (eissect h b)^)
@' eissect k (g (h^-1 (h b)))
@' ap g (eissect h b) = eissect k (g b)
    all:rewrite <- (ap_compose (k o _) k^-1), (ap_compose _ (k^-1 o k)).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
ap (fun x : A => k^-1 (k x)) (ap f (eissect h b)^)
@' eissect k (f (h^-1 (h b)))
@' ap f (eissect h b) = eissect k (f b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
ap (fun x : A => k^-1 (k x)) (ap g (eissect h b)^)
@' eissect k (g (h^-1 (h b)))
@' ap g (eissect h b) = eissect k (g b)
    all:rewrite (concat_A1p (eissect k) _).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
eissect k (f b)
@' ap f (eissect h b)^
@' ap f (eissect h b) = eissect k (f b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
H: IsEquiv h
H0: IsEquiv k
p: k o f == f' o h
q: k o g == g' o h
b: B
eissect k (g b)
@' ap g (eissect h b)^
@' ap g (eissect h b) = eissect k (g b)
    all:rewrite ap_V, concat_pV_p; reflexivity.
    Close Scope long_path_scope.
  Qed.

  #[export] Instance isequiv_functor_coeq
  : IsEquiv (functor_coeq h k p q)
    := isequiv_adjointify _ functor_coeq_inverse
                          functor_coeq_eissect functor_coeq_eisretr.

  Definition equiv_functor_coeq
  : @Coeq B A f g <~> @Coeq B' A' f' g'
    := Build_Equiv _ _ (functor_coeq h k p q) _.

End IsEquivFunctorCoeq.

Definition equiv_functor_coeq' {B A f g B' A' f' g'}
           (h : B <~> B') (k : A <~> A')
           (p : k o f == f' o h) (q : k o g == g' o h)
: @Coeq B A f g <~> @Coeq B' A' f' g'
  := equiv_functor_coeq h k p q.

(** ** A double recursion principle *)

Section CoeqRec2.
  Context {B A : Type} {f g : B -> A} {B' A' : Type} {f' g' : B' -> A'}
    (P : Type) (coeq' : A -> A' -> P)
    (cgluel : forall b a', coeq' (f b) a' = coeq' (g b) a')
    (cgluer : forall a b', coeq' a (f' b') = coeq' a (g' b'))
    (cgluelr : forall b b', cgluel b (f' b') @ cgluer (g b) b'
                          = cgluer (f b) b' @ cgluel b (g' b')).

  Definition Coeq_rec2 : Coeq f g -> Coeq f' g' -> P.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
Coeq f g -> Coeq f' g' -> P
  Proof.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
Coeq f g -> Coeq f' g' -> P
    intros x y; revert x.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
y: Coeq f' g'
Coeq f g -> P
    snapply Coeq_rec.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
y: Coeq f' g'
A -> P
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
y: Coeq f' g'
forall b : B, ?coeq' (f b) = ?coeq' (g b)
    -
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
y: Coeq f' g'
A -> P intros a.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
y: Coeq f' g'
a: A
P
      revert y.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
a: A
Coeq f' g' -> P
      snapply Coeq_rec.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
a: A
A' -> P
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
a: A
forall b : B', ?coeq' (f' b) = ?coeq' (g' b)
      +
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
a: A
A' -> P intros a'.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
a: A
a': A'
P
        exact (coeq' a a').
      +
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
a: A
forall b : B',
(fun a' : A' => coeq' a a') (f' b) =
(fun a' : A' => coeq' a a') (g' b) intros b'; cbn.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
a: A
b': B'
coeq' a (f' b') = coeq' a (g' b')
        apply cgluer.
    -
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
y: Coeq f' g'
forall b : B,
(fun a : A =>
 Coeq_rec P (fun a' : A' => coeq' a a')
   (fun b' : B' =>
    cgluer a b'
    :
    (fun a' : A' => coeq' a a') (f' b') =
    (fun a' : A' => coeq' a a') (g' b')) y) (f b) =
(fun a : A =>
 Coeq_rec P (fun a' : A' => coeq' a a')
   (fun b' : B' =>
    cgluer a b'
    :
    (fun a' : A' => coeq' a a') (f' b') =
    (fun a' : A' => coeq' a a') (g' b')) y) (g b) intros b.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
y: Coeq f' g'
b: B
(fun a : A =>
 Coeq_rec P (fun a' : A' => coeq' a a')
   (fun b' : B' =>
    cgluer a b'
    :
    (fun a' : A' => coeq' a a') (f' b') =
    (fun a' : A' => coeq' a a') (g' b')) y) (f b) =
(fun a : A =>
 Coeq_rec P (fun a' : A' => coeq' a a')
   (fun b' : B' =>
    cgluer a b'
    :
    (fun a' : A' => coeq' a a') (f' b') =
    (fun a' : A' => coeq' a a') (g' b')) y) (g b)
      revert y.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
forall y : Coeq f' g',
(fun a : A =>
 Coeq_rec P (fun a' : A' => coeq' a a')
   (fun b' : B' =>
    cgluer a b'
    :
    (fun a' : A' => coeq' a a') (f' b') =
    (fun a' : A' => coeq' a a') (g' b')) y) (f b) =
(fun a : A =>
 Coeq_rec P (fun a' : A' => coeq' a a')
   (fun b' : B' =>
    cgluer a b'
    :
    (fun a' : A' => coeq' a a') (f' b') =
    (fun a' : A' => coeq' a a') (g' b')) y) (g b)
      snapply Coeq_ind.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
forall a : A',
(fun w : Coeq f' g' =>
 (fun a0 : A =>
  Coeq_rec P (fun a' : A' => coeq' a0 a')
    (fun b' : B' =>
     cgluer a0 b'
     :
     (fun a' : A' => coeq' a0 a') (f' b') =
     (fun a' : A' => coeq' a0 a') (g' b')) w) (f b) =
 (fun a0 : A =>
  Coeq_rec P (fun a' : A' => coeq' a0 a')
    (fun b' : B' =>
     cgluer a0 b'
     :
     (fun a' : A' => coeq' a0 a') (f' b') =
     (fun a' : A' => coeq' a0 a') (g' b')) w) (g b))
  (coeq a)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
forall b0 : B',
transport
  (fun w : Coeq f' g' =>
   (fun a : A =>
    Coeq_rec P (fun a' : A' => coeq' a a')
      (fun b' : B' =>
       cgluer a b'
       :
       (fun a' : A' => coeq' a a') (f' b') =
       (fun a' : A' => coeq' a a') (g' b')) w) 
     (f b) =
   (fun a : A =>
    Coeq_rec P (fun a' : A' => coeq' a a')
      (fun b' : B' =>
       cgluer a b'
       :
       (fun a' : A' => coeq' a a') (f' b') =
       (fun a' : A' => coeq' a a') (g' b')) w) 
     (g b)) (cglue b0) (?coeq' (f' b0)) =
?coeq' (g' b0)
      +
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
forall a : A',
(fun w : Coeq f' g' =>
 (fun a0 : A =>
  Coeq_rec P (fun a' : A' => coeq' a0 a')
    (fun b' : B' =>
     cgluer a0 b'
     :
     (fun a' : A' => coeq' a0 a') (f' b') =
     (fun a' : A' => coeq' a0 a') (g' b')) w) (f b) =
 (fun a0 : A =>
  Coeq_rec P (fun a' : A' => coeq' a0 a')
    (fun b' : B' =>
     cgluer a0 b'
     :
     (fun a' : A' => coeq' a0 a') (f' b') =
     (fun a' : A' => coeq' a0 a') (g' b')) w) (g b))
  (coeq a) intros a'.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
a': A'
(fun w : Coeq f' g' =>
 (fun a : A =>
  Coeq_rec P (fun a' : A' => coeq' a a')
    (fun b' : B' =>
     cgluer a b'
     :
     (fun a' : A' => coeq' a a') (f' b') =
     (fun a' : A' => coeq' a a') (g' b')) w) (f b) =
 (fun a : A =>
  Coeq_rec P (fun a' : A' => coeq' a a')
    (fun b' : B' =>
     cgluer a b'
     :
     (fun a' : A' => coeq' a a') (f' b') =
     (fun a' : A' => coeq' a a') (g' b')) w) (g b))
  (coeq a')
        cbn.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
a': A'
Coeq_rec P (fun a' : A' => coeq' (f b) a')
  (fun b' : B' => cgluer (f b) b') (coeq a') =
Coeq_rec P (fun a' : A' => coeq' (g b) a')
  (fun b' : B' => cgluer (g b) b') (coeq a')
        apply cgluel.
      +
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
forall b0 : B',
transport
  (fun w : Coeq f' g' =>
   (fun a : A =>
    Coeq_rec P (fun a' : A' => coeq' a a')
      (fun b' : B' =>
       cgluer a b'
       :
       (fun a' : A' => coeq' a a') (f' b') =
       (fun a' : A' => coeq' a a') (g' b')) w) (f b) =
   (fun a : A =>
    Coeq_rec P (fun a' : A' => coeq' a a')
      (fun b' : B' =>
       cgluer a b'
       :
       (fun a' : A' => coeq' a a') (f' b') =
       (fun a' : A' => coeq' a a') (g' b')) w) (g b))
  (cglue b0)
  ((fun a' : A' =>
    cgluel b a'
    :
    (fun w : Coeq f' g' =>
     (fun a : A =>
      Coeq_rec P (fun a'0 : A' => coeq' a a'0)
        (fun b' : B' =>
         cgluer a b'
         :
         (fun a'0 : A' => coeq' a a'0) (f' b') =
         (fun a'0 : A' => coeq' a a'0) (g' b')) w)
       (f b) =
     (fun a : A =>
      Coeq_rec P (fun a'0 : A' => coeq' a a'0)
        (fun b' : B' =>
         cgluer a b'
         :
         (fun a'0 : A' => coeq' a a'0) (f' b') =
         (fun a'0 : A' => coeq' a a'0) (g' b')) w)
       (g b)) (coeq a')) (f' b0)) =
(fun a' : A' =>
 cgluel b a'
 :
 (fun w : Coeq f' g' =>
  (fun a : A =>
   Coeq_rec P (fun a'0 : A' => coeq' a a'0)
     (fun b' : B' =>
      cgluer a b'
      :
      (fun a'0 : A' => coeq' a a'0) (f' b') =
      (fun a'0 : A' => coeq' a a'0) (g' b')) w) (f b) =
  (fun a : A =>
   Coeq_rec P (fun a'0 : A' => coeq' a a'0)
     (fun b' : B' =>
      cgluer a b'
      :
      (fun a'0 : A' => coeq' a a'0) (f' b') =
      (fun a'0 : A' => coeq' a a'0) (g' b')) w) (g b))
   (coeq a')) (g' b0) intros b'.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
b': B'
transport
  (fun w : Coeq f' g' =>
   (fun a : A =>
    Coeq_rec P (fun a' : A' => coeq' a a')
      (fun b' : B' =>
       cgluer a b'
       :
       (fun a' : A' => coeq' a a') (f' b') =
       (fun a' : A' => coeq' a a') (g' b')) w) (f b) =
   (fun a : A =>
    Coeq_rec P (fun a' : A' => coeq' a a')
      (fun b' : B' =>
       cgluer a b'
       :
       (fun a' : A' => coeq' a a') (f' b') =
       (fun a' : A' => coeq' a a') (g' b')) w) (g b))
  (cglue b')
  ((fun a' : A' =>
    cgluel b a'
    :
    (fun w : Coeq f' g' =>
     (fun a : A =>
      Coeq_rec P (fun a'0 : A' => coeq' a a'0)
        (fun b' : B' =>
         cgluer a b'
         :
         (fun a'0 : A' => coeq' a a'0) (f' b') =
         (fun a'0 : A' => coeq' a a'0) (g' b')) w)
       (f b) =
     (fun a : A =>
      Coeq_rec P (fun a'0 : A' => coeq' a a'0)
        (fun b' : B' =>
         cgluer a b'
         :
         (fun a'0 : A' => coeq' a a'0) (f' b') =
         (fun a'0 : A' => coeq' a a'0) (g' b')) w)
       (g b)) (coeq a')) (f' b')) =
(fun a' : A' =>
 cgluel b a'
 :
 (fun w : Coeq f' g' =>
  (fun a : A =>
   Coeq_rec P (fun a'0 : A' => coeq' a a'0)
     (fun b' : B' =>
      cgluer a b'
      :
      (fun a'0 : A' => coeq' a a'0) (f' b') =
      (fun a'0 : A' => coeq' a a'0) (g' b')) w) (f b) =
  (fun a : A =>
   Coeq_rec P (fun a'0 : A' => coeq' a a'0)
     (fun b' : B' =>
      cgluer a b'
      :
      (fun a'0 : A' => coeq' a a'0) (f' b') =
      (fun a'0 : A' => coeq' a a'0) (g' b')) w) (g b))
   (coeq a')) (g' b')
        transport_paths (transport_paths_FlFr (cglue b')).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
b': B'
ap
  (Coeq_rec P (fun a' : A' => coeq' (f b) a')
     (fun b' : B' => cgluer (f b) b')) (cglue b') @
cgluel b (g' b') =
cgluel b (f' b') @
ap
  (Coeq_rec P (fun a' : A' => coeq' (g b) a')
     (fun b' : B' => cgluer (g b) b')) (cglue b')
        lhs napply (_ @@ 1).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
b': B'
ap
  (Coeq_rec P (fun a' : A' => coeq' (f b) a')
     (fun b' : B' => cgluer (f b) b')) (cglue b') =
?Goal
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
b': B'
?Goal @ cgluel b (g' b') =
cgluel b (f' b') @
ap
  (Coeq_rec P (fun a' : A' => coeq' (g b) a')
     (fun b' : B' => cgluer (g b) b')) 
  (cglue b')
        1: apply Coeq_rec_beta_cglue.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
b': B'
cgluer (f b) b' @ cgluel b (g' b') =
cgluel b (f' b') @
ap
  (Coeq_rec P (fun a' : A' => coeq' (g b) a')
     (fun b' : B' => cgluer (g b) b')) (cglue b')
        rhs napply (1 @@ _).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
b': B'
cgluer (f b) b' @ cgluel b (g' b') =
cgluel b (f' b') @ ?Goal
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
b': B'
ap
  (Coeq_rec P (fun a' : A' => coeq' (g b) a')
     (fun b' : B' => cgluer (g b) b')) 
  (cglue b') = ?Goal
        2: apply Coeq_rec_beta_cglue.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
b': B'
cgluer (f b) b' @ cgluel b (g' b') =
cgluel b (f' b') @ cgluer (g b) b'
        symmetry.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
b': B'
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
        apply cgluelr.
  Defined.

  Definition Coeq_rec2_beta (a : A) (a' : A')
    : Coeq_rec2 (coeq a) (coeq a') = coeq' a a'
    := 1.

  Definition Coeq_rec2_beta_cgluel (a : A) (b' : B')
    : ap (Coeq_rec2 (coeq a)) (cglue b') = cgluer a b'.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
a: A
b': B'
ap (Coeq_rec2 (coeq a)) (cglue b') = cgluer a b'
  Proof.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
a: A
b': B'
ap (Coeq_rec2 (coeq a)) (cglue b') = cgluer a b'
    napply Coeq_rec_beta_cglue.
  Defined.

  Definition Coeq_rec2_beta_cgluer (b : B) (a' : A')
    : ap (fun x => Coeq_rec2 x (coeq a')) (cglue b) = cgluel b a'.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
a': A'
ap (fun x : Coeq f g => Coeq_rec2 x (coeq a'))
  (cglue b) = cgluel b a'
  Proof.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Type
coeq': A -> A' -> P
cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
b: B
a': A'
ap (fun x : Coeq f g => Coeq_rec2 x (coeq a'))
  (cglue b) = cgluel b a'
    napply Coeq_rec_beta_cglue.
  Defined.

  (** TODO: [Coeq_rec2_beta_cgluelr] *)

End CoeqRec2.

(** ** A double induction principle *)

Section CoeqInd2.
  Context `{Funext}
          {B A : Type} {f g : B -> A} {B' A' : Type} {f' g' : B' -> A'}
          (P : Coeq f g -> Coeq f' g' -> Type)
          (coeq' : forall a a', P (coeq a) (coeq a'))
          (cgluel : forall b a',
                   transport (fun x => P x (coeq a')) (cglue b)
                             (coeq' (f b) a') = coeq' (g b) a')
          (cgluer : forall a b',
                   transport (fun y => P (coeq a) y) (cglue b')
                             (coeq' a (f' b')) = coeq' a (g' b'))
          (** Perhaps this should really be written using [concatD]. *)
          (cgluelr : forall b b',
                  ap (transport (P (coeq (g b))) (cglue b')) (cgluel b (f' b'))
                  @ cgluer (g b) b'
                  = transport_transport P (cglue b) (cglue b') (coeq' (f b) (f' b'))
                  @ ap (transport (fun x => P x (coeq (g' b'))) (cglue b))
                       (cgluer (f b) b')
                  @ cgluel b (g' b')).

  Definition Coeq_ind2
  : forall x y, P x y.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
forall (x : Coeq f g) (y : Coeq f' g'), P x y
  Proof.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
forall (x : Coeq f g) (y : Coeq f' g'), P x y
    simple refine (Coeq_ind _ _ _).
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
forall a : A,
(fun w : Coeq f g => forall y : Coeq f' g', P w y)
  (coeq a)
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
forall b : B,
transport
  (fun w : Coeq f g => forall y : Coeq f' g', P w y)
  (cglue b) (?coeq' (f b)) = 
?coeq' (g b)
    -
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
forall a : A,
(fun w : Coeq f g => forall y : Coeq f' g', P w y)
  (coeq a) intros a.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
a: A
(fun w : Coeq f g => forall y : Coeq f' g', P w y)
  (coeq a)
      simple refine (Coeq_ind _ _ _).
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
a: A
forall a0 : A', P (coeq a) (coeq a0)
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
a: A
forall b : B',
transport (P (coeq a)) (cglue b) (?coeq' (f' b)) =
?coeq' (g' b)
      +
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
a: A
forall a0 : A', P (coeq a) (coeq a0) intros a'.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
a: A
a': A'
P (coeq a) (coeq a')
        exact (coeq' a a').
      +
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
a: A
forall b : B',
transport (P (coeq a)) (cglue b)
  ((fun a' : A' => coeq' a a') (f' b)) =
(fun a' : A' => coeq' a a') (g' b) intros b'; cbn.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
a: A
b': B'
transport (P (coeq a)) (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
        apply cgluer.
    -
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
forall b : B,
transport
  (fun w : Coeq f g => forall y : Coeq f' g', P w y)
  (cglue b)
  ((fun a : A =>
    Coeq_ind (P (coeq a)) (fun a' : A' => coeq' a a')
      (fun b' : B' =>
       cgluer a b'
       :
       transport (P (coeq a)) (cglue b')
         ((fun a' : A' => coeq' a a') (f' b')) =
       (fun a' : A' => coeq' a a') (g' b'))) (f b)) =
(fun a : A =>
 Coeq_ind (P (coeq a)) (fun a' : A' => coeq' a a')
   (fun b' : B' =>
    cgluer a b'
    :
    transport (P (coeq a)) (cglue b')
      ((fun a' : A' => coeq' a a') (f' b')) =
    (fun a' : A' => coeq' a a') (g' b'))) (g b) intros b.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
b: B
transport
  (fun w : Coeq f g => forall y : Coeq f' g', P w y)
  (cglue b)
  ((fun a : A =>
    Coeq_ind (P (coeq a)) (fun a' : A' => coeq' a a')
      (fun b' : B' =>
       cgluer a b'
       :
       transport (P (coeq a)) (cglue b')
         ((fun a' : A' => coeq' a a') (f' b')) =
       (fun a' : A' => coeq' a a') (g' b'))) (f b)) =
(fun a : A =>
 Coeq_ind (P (coeq a)) (fun a' : A' => coeq' a a')
   (fun b' : B' =>
    cgluer a b'
    :
    transport (P (coeq a)) (cglue b')
      ((fun a' : A' => coeq' a a') (f' b')) =
    (fun a' : A' => coeq' a a') (g' b'))) (g b)
      apply path_forall; intros a.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
b: B
a: Coeq f' g'
transport
  (fun w : Coeq f g => forall y : Coeq f' g', P w y)
  (cglue b)
  (Coeq_ind (P (coeq (f b)))
     (fun a' : A' => coeq' (f b) a')
     (fun b' : B' => cgluer (f b) b')) a =
Coeq_ind (P (coeq (g b)))
  (fun a' : A' => coeq' (g b) a')
  (fun b' : B' => cgluer (g b) b') a
      revert a; simple refine (Coeq_ind _ _ _).
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
b: B
forall a : A',
(fun w : Coeq f' g' =>
 transport
   (fun w0 : Coeq f g => forall y : Coeq f' g', P w0 y)
   (cglue b)
   (Coeq_ind (P (coeq (f b)))
      (fun a' : A' => coeq' (f b) a')
      (fun b' : B' => cgluer (f b) b')) w =
 Coeq_ind (P (coeq (g b)))
   (fun a' : A' => coeq' (g b) a')
   (fun b' : B' => cgluer (g b) b') w) (coeq a)
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
b: B
forall b0 : B',
transport
  (fun w : Coeq f' g' =>
   transport
     (fun w0 : Coeq f g =>
      forall y : Coeq f' g', P w0 y) 
     (cglue b)
     (Coeq_ind (P (coeq (f b)))
        (fun a' : A' => coeq' (f b) a')
        (fun b' : B' => cgluer (f b) b')) w =
   Coeq_ind (P (coeq (g b)))
     (fun a' : A' => coeq' (g b) a')
     (fun b' : B' => cgluer (g b) b') w) 
  (cglue b0) (?coeq' (f' b0)) = 
?coeq' (g' b0)
      +
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
b: B
forall a : A',
(fun w : Coeq f' g' =>
 transport
   (fun w0 : Coeq f g => forall y : Coeq f' g', P w0 y)
   (cglue b)
   (Coeq_ind (P (coeq (f b)))
      (fun a' : A' => coeq' (f b) a')
      (fun b' : B' => cgluer (f b) b')) w =
 Coeq_ind (P (coeq (g b)))
   (fun a' : A' => coeq' (g b) a')
   (fun b' : B' => cgluer (g b) b') w) (coeq a) intros a'.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
b: B
a': A'
(fun w : Coeq f' g' =>
 transport
   (fun w0 : Coeq f g => forall y : Coeq f' g', P w0 y)
   (cglue b)
   (Coeq_ind (P (coeq (f b)))
      (fun a' : A' => coeq' (f b) a')
      (fun b' : B' => cgluer (f b) b')) w =
 Coeq_ind (P (coeq (g b)))
   (fun a' : A' => coeq' (g b) a')
   (fun b' : B' => cgluer (g b) b') w) (coeq a') cbn.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
b: B
a': A'
transport
  (fun w : Coeq f g => forall y : Coeq f' g', P w y)
  (cglue b)
  (Coeq_ind (P (coeq (f b)))
     (fun a' : A' => coeq' (f b) a')
     (fun b' : B' => cgluer (f b) b')) (coeq a') =
Coeq_ind (P (coeq (g b)))
  (fun a' : A' => coeq' (g b) a')
  (fun b' : B' => cgluer (g b) b') (coeq a')
        refine (transport_forall_constant _ _ _ @ _).
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
b: B
a': A'
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b)
  (Coeq_ind (P (coeq (f b)))
     (fun a' : A' => coeq' (f b) a')
     (fun b' : B' => cgluer (f b) b') (coeq a')) =
Coeq_ind (P (coeq (g b)))
  (fun a' : A' => coeq' (g b) a')
  (fun b' : B' => cgluer (g b) b') (coeq a')
        apply cgluel.
      +
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
b: B
forall b0 : B',
transport
  (fun w : Coeq f' g' =>
   transport
     (fun w0 : Coeq f g =>
      forall y : Coeq f' g', P w0 y) (cglue b)
     (Coeq_ind (P (coeq (f b)))
        (fun a' : A' => coeq' (f b) a')
        (fun b' : B' => cgluer (f b) b')) w =
   Coeq_ind (P (coeq (g b)))
     (fun a' : A' => coeq' (g b) a')
     (fun b' : B' => cgluer (g b) b') w) (cglue b0)
  ((fun a' : A' =>
    transport_forall_constant (cglue b)
      (Coeq_ind (P (coeq (f b)))
         (fun a'0 : A' => coeq' (f b) a'0)
         (fun b' : B' => cgluer (f b) b')) (coeq a') @
    cgluel b a'
    :
    (fun w : Coeq f' g' =>
     transport
       (fun w0 : Coeq f g =>
        forall y : Coeq f' g', P w0 y) (cglue b)
       (Coeq_ind (P (coeq (f b)))
          (fun a'0 : A' => coeq' (f b) a'0)
          (fun b' : B' => cgluer (f b) b')) w =
     Coeq_ind (P (coeq (g b)))
       (fun a'0 : A' => coeq' (g b) a'0)
       (fun b' : B' => cgluer (g b) b') w) (coeq a'))
     (f' b0)) =
(fun a' : A' =>
 transport_forall_constant (cglue b)
   (Coeq_ind (P (coeq (f b)))
      (fun a'0 : A' => coeq' (f b) a'0)
      (fun b' : B' => cgluer (f b) b')) (coeq a') @
 cgluel b a'
 :
 (fun w : Coeq f' g' =>
  transport
    (fun w0 : Coeq f g =>
     forall y : Coeq f' g', P w0 y) (cglue b)
    (Coeq_ind (P (coeq (f b)))
       (fun a'0 : A' => coeq' (f b) a'0)
       (fun b' : B' => cgluer (f b) b')) w =
  Coeq_ind (P (coeq (g b)))
    (fun a'0 : A' => coeq' (g b) a'0)
    (fun b' : B' => cgluer (g b) b') w) (coeq a'))
  (g' b0) intros b'; cbn.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
b: B
b': B'
transport
  (fun w : Coeq f' g' =>
   transport
     (fun w0 : Coeq f g =>
      forall y : Coeq f' g', P w0 y) (cglue b)
     (Coeq_ind (P (coeq (f b)))
        (fun a' : A' => coeq' (f b) a')
        (fun b' : B' => cgluer (f b) b')) w =
   Coeq_ind (P (coeq (g b)))
     (fun a' : A' => coeq' (g b) a')
     (fun b' : B' => cgluer (g b) b') w) (cglue b')
  (transport_forall_constant (cglue b)
     (Coeq_ind (P (coeq (f b)))
        (fun a' : A' => coeq' (f b) a')
        (fun b' : B' => cgluer (f b) b'))
     (coeq (f' b')) @ cgluel b (f' b')) =
transport_forall_constant (cglue b)
  (Coeq_ind (P (coeq (f b)))
     (fun a' : A' => coeq' (f b) a')
     (fun b' : B' => cgluer (f b) b')) (coeq (g' b')) @
cgluel b (g' b')
        refine (transport_paths_FlFr_D (cglue b') _ @ _).
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
b: B
b': B'
((apD
    (transport
       (fun w : Coeq f g =>
        forall y : Coeq f' g', P w y) (cglue b)
       (Coeq_ind (P (coeq (f b)))
          (fun a' : A' => coeq' (f b) a')
          (fun b' : B' => cgluer (f b) b')))
    (cglue b'))^ @
 ap (transport (P (coeq (g b))) (cglue b'))
   (transport_forall_constant (cglue b)
      (Coeq_ind (P (coeq (f b)))
         (fun a' : A' => coeq' (f b) a')
         (fun b' : B' => cgluer (f b) b'))
      (coeq (f' b')) @ cgluel b (f' b'))) @
apD
  (Coeq_ind (P (coeq (g b)))
     (fun a' : A' => coeq' (g b) a')
     (fun b' : B' => cgluer (g b) b')) (cglue b') =
transport_forall_constant (cglue b)
  (Coeq_ind (P (coeq (f b)))
     (fun a' : A' => coeq' (f b) a')
     (fun b' : B' => cgluer (f b) b')) (coeq (g' b')) @
cgluel b (g' b')
        rewrite Coeq_ind_beta_cglue.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b) 
   (cglue b') (coeq' (f b) (f' b')) @
 ap
   (transport
      (fun x : Coeq f g =>
       P x (coeq (g' b'))) 
      (cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
b: B
b': B'
((apD
    (transport
       (fun w : Coeq f g =>
        forall y : Coeq f' g', P w y) (cglue b)
       (Coeq_ind (P (coeq (f b)))
          (fun a' : A' => coeq' (f b) a')
          (fun b' : B' => cgluer (f b) b')))
    (cglue b'))^ @
 ap (transport (P (coeq (g b))) (cglue b'))
   (transport_forall_constant (cglue b)
      (Coeq_ind (P (coeq (f b)))
         (fun a' : A' => coeq' (f b) a')
         (fun b' : B' => cgluer (f b) b'))
      (coeq (f' b')) @ cgluel b (f' b'))) @
cgluer (g b) b' =
transport_forall_constant (cglue b)
  (Coeq_ind (P (coeq (f b)))
     (fun a' : A' => coeq' (f b) a')
     (fun b' : B' => cgluer (f b) b')) (coeq (g' b')) @
cgluel b (g' b')
        (** Now begins the long haul. *)
        Open Scope long_path_scope.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b) 
  (cglue b') (coeq' (f b) (f' b'))
@' ap
     (transport
        (fun x : Coeq f g =>
         P x (coeq (g' b'))) 
        (cglue b)) (cgluer (f b) b')
@' cgluel b (g' b')
b: B
b': B'
(apD
   (transport
      (fun w : Coeq f g =>
       forall y : Coeq f' g', P w y) (cglue b)
      (Coeq_ind (P (coeq (f b)))
         (fun a' : A' => coeq' (f b) a')
         (fun b' : B' => cgluer (f b) b'))) (cglue b'))^
@' ap (transport (P (coeq (g b))) (cglue b'))
     (transport_forall_constant (cglue b)
        (Coeq_ind (P (coeq (f b)))
           (fun a' : A' => coeq' (f b) a')
           (fun b' : B' => cgluer (f b) b'))
        (coeq (f' b'))
      @' cgluel b (f' b'))
@' cgluer (g b) b' =
transport_forall_constant (cglue b)
  (Coeq_ind (P (coeq (f b)))
     (fun a' : A' => coeq' (f b) a')
     (fun b' : B' => cgluer (f b) b')) (coeq (g' b'))
@' cgluel b (g' b')
        rewrite ap_pp.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b) 
  (cglue b') (coeq' (f b) (f' b'))
@' ap
     (transport
        (fun x : Coeq f g =>
         P x (coeq (g' b'))) 
        (cglue b)) (cgluer (f b) b')
@' cgluel b (g' b')
b: B
b': B'
(apD
   (transport
      (fun w : Coeq f g =>
       forall y : Coeq f' g', P w y) (cglue b)
      (Coeq_ind (P (coeq (f b)))
         (fun a' : A' => coeq' (f b) a')
         (fun b' : B' => cgluer (f b) b'))) (cglue b'))^
@' (ap (transport (P (coeq (g b))) (cglue b'))
      (transport_forall_constant (cglue b)
         (Coeq_ind (P (coeq (f b)))
            (fun a' : A' => coeq' (f b) a')
            (fun b' : B' => cgluer (f b) b'))
         (coeq (f' b')))
    @' ap (transport (P (coeq (g b))) (cglue b'))
         (cgluel b (f' b')))
@' cgluer (g b) b' =
transport_forall_constant (cglue b)
  (Coeq_ind (P (coeq (f b)))
     (fun a' : A' => coeq' (f b) a')
     (fun b' : B' => cgluer (f b) b')) (coeq (g' b'))
@' cgluel b (g' b')
        repeat rewrite concat_p_pp.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b) 
  (cglue b') (coeq' (f b) (f' b'))
@' ap
     (transport
        (fun x : Coeq f g =>
         P x (coeq (g' b'))) 
        (cglue b)) (cgluer (f b) b')
@' cgluel b (g' b')
b: B
b': B'
(apD
   (transport
      (fun w : Coeq f g =>
       forall y : Coeq f' g', P w y) (cglue b)
      (Coeq_ind (P (coeq (f b)))
         (fun a' : A' => coeq' (f b) a')
         (fun b' : B' => cgluer (f b) b'))) (cglue b'))^
@' ap (transport (P (coeq (g b))) (cglue b'))
     (transport_forall_constant (cglue b)
        (Coeq_ind (P (coeq (f b)))
           (fun a' : A' => coeq' (f b) a')
           (fun b' : B' => cgluer (f b) b'))
        (coeq (f' b')))
@' ap (transport (P (coeq (g b))) (cglue b'))
     (cgluel b (f' b'))
@' cgluer (g b) b' =
transport_forall_constant (cglue b)
  (Coeq_ind (P (coeq (f b)))
     (fun a' : A' => coeq' (f b) a')
     (fun b' : B' => cgluer (f b) b')) (coeq (g' b'))
@' cgluel b (g' b')
        (** Our first order of business is to get rid of the [Coeq_ind]s, which only occur in the following incarnation. *)
        set (G := (Coeq_ind (P (coeq (f b)))
                            (fun a' : A' => coeq' (f b) a')
                            (fun b'0 : B' => cgluer (f b) b'0))).
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b) 
  (cglue b') (coeq' (f b) (f' b'))
@' ap
     (transport
        (fun x : Coeq f g =>
         P x (coeq (g' b'))) 
        (cglue b)) (cgluer (f b) b')
@' cgluel b (g' b')
b: B
b': B'
G:= Coeq_ind (P (coeq (f b)))
  (fun a' : A' => coeq' (f b) a')
  (fun b'0 : B' => cgluer (f b) b'0): forall w : Coeq f' g', P (coeq (f b)) w
(apD
   (transport
      (fun w : Coeq f g =>
       forall y : Coeq f' g', P w y) (cglue b) G)
   (cglue b'))^
@' ap (transport (P (coeq (g b))) (cglue b'))
     (transport_forall_constant (cglue b) G
        (coeq (f' b')))
@' ap (transport (P (coeq (g b))) (cglue b'))
     (cgluel b (f' b'))
@' cgluer (g b) b' =
transport_forall_constant (cglue b) G (coeq (g' b'))
@' cgluel b (g' b')
        (** Let's reduce the [apD (loop # G)] first. *)
        rewrite (apD_transport_forall_constant P (cglue b) G (cglue b')); simpl.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b) 
  (cglue b') (coeq' (f b) (f' b'))
@' ap
     (transport
        (fun x : Coeq f g =>
         P x (coeq (g' b'))) 
        (cglue b)) (cgluer (f b) b')
@' cgluel b (g' b')
b: B
b': B'
G:= Coeq_ind (P (coeq (f b)))
  (fun a' : A' => coeq' (f b) a')
  (fun b'0 : B' => cgluer (f b) b'0): forall w : Coeq f' g', P (coeq (f b)) w
(ap (transport (P (coeq (g b))) (cglue b'))
   (transport_forall_constant (cglue b) G
      (coeq (f' b')))
 @' transport_transport P (cglue b) (cglue b')
      (coeq' (f b) (f' b'))
 @' ap
      (transport
         (fun x : Coeq f g => P x (coeq (g' b')))
         (cglue b)) (apD G (cglue b'))
 @' (transport_forall_constant (cglue b) G
       (coeq (g' b')))^)^
@' ap (transport (P (coeq (g b))) (cglue b'))
     (transport_forall_constant (cglue b) G
        (coeq (f' b')))
@' ap (transport (P (coeq (g b))) (cglue b'))
     (cgluel b (f' b'))
@' cgluer (g b) b' =
transport_forall_constant (cglue b) G (coeq (g' b'))
@' cgluel b (g' b')
        rewrite !inv_pp, !inv_V.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b) 
  (cglue b') (coeq' (f b) (f' b'))
@' ap
     (transport
        (fun x : Coeq f g =>
         P x (coeq (g' b'))) 
        (cglue b)) (cgluer (f b) b')
@' cgluel b (g' b')
b: B
b': B'
G:= Coeq_ind (P (coeq (f b)))
  (fun a' : A' => coeq' (f b) a')
  (fun b'0 : B' => cgluer (f b) b'0): forall w : Coeq f' g', P (coeq (f b)) w
transport_forall_constant (cglue b) G (coeq (g' b'))
@' ((ap
       (transport
          (fun x : Coeq f g => P x (coeq (g' b')))
          (cglue b)) (apD G (cglue b')))^
    @' ((transport_transport P (cglue b) (cglue b')
           (coeq' (f b) (f' b')))^
        @' (ap (transport (P (coeq (g b))) (cglue b'))
              (transport_forall_constant (cglue b) G
                 (coeq (f' b'))))^))
@' ap (transport (P (coeq (g b))) (cglue b'))
     (transport_forall_constant (cglue b) G
        (coeq (f' b')))
@' ap (transport (P (coeq (g b))) (cglue b'))
     (cgluel b (f' b'))
@' cgluer (g b) b' =
transport_forall_constant (cglue b) G (coeq (g' b'))
@' cgluel b (g' b')
        (** Now we can cancel a [transport_forall_constant]. *)
        rewrite !concat_pp_p; apply whiskerL.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b) 
  (cglue b') (coeq' (f b) (f' b'))
@' ap
     (transport
        (fun x : Coeq f g =>
         P x (coeq (g' b'))) 
        (cglue b)) (cgluer (f b) b')
@' cgluel b (g' b')
b: B
b': B'
G:= Coeq_ind (P (coeq (f b)))
  (fun a' : A' => coeq' (f b) a')
  (fun b'0 : B' => cgluer (f b) b'0): forall w : Coeq f' g', P (coeq (f b)) w
(ap
   (transport (fun x : Coeq f g => P x (coeq (g' b')))
      (cglue b)) (apD G (cglue b')))^
@' ((transport_transport P (cglue b) (cglue b')
       (coeq' (f b) (f' b')))^
    @' ((ap (transport (P (coeq (g b))) (cglue b'))
           (transport_forall_constant (cglue b) G
              (coeq (f' b'))))^
        @' (ap (transport (P (coeq (g b))) (cglue b'))
              (transport_forall_constant (cglue b) G
                 (coeq (f' b')))
            @' (ap
                  (transport (P (coeq (g b)))
                     (cglue b')) (cgluel b (f' b'))
                @' cgluer (g b) b')))) =
cgluel b (g' b')
        (** And a path-inverse pair.  This removes all the [transport_forall_constant]s. *)
        rewrite !concat_p_pp, concat_pV_p.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b) 
  (cglue b') (coeq' (f b) (f' b'))
@' ap
     (transport
        (fun x : Coeq f g =>
         P x (coeq (g' b'))) 
        (cglue b)) (cgluer (f b) b')
@' cgluel b (g' b')
b: B
b': B'
G:= Coeq_ind (P (coeq (f b)))
  (fun a' : A' => coeq' (f b) a')
  (fun b'0 : B' => cgluer (f b) b'0): forall w : Coeq f' g', P (coeq (f b)) w
(ap
   (transport (fun x : Coeq f g => P x (coeq (g' b')))
      (cglue b)) (apD G (cglue b')))^
@' (transport_transport P (cglue b) (cglue b')
      (coeq' (f b) (f' b')))^
@' ap (transport (P (coeq (g b))) (cglue b'))
     (cgluel b (f' b'))
@' cgluer (g b) b' = cgluel b (g' b')
        (** Now we can beta-reduce the last remaining [G]. *)
        subst G; rewrite Coeq_ind_beta_cglue; simpl.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b) 
  (cglue b') (coeq' (f b) (f' b'))
@' ap
     (transport
        (fun x : Coeq f g =>
         P x (coeq (g' b'))) 
        (cglue b)) (cgluer (f b) b')
@' cgluel b (g' b')
b: B
b': B'
(ap
   (transport (fun x : Coeq f g => P x (coeq (g' b')))
      (cglue b)) (cgluer (f b) b'))^
@' (transport_transport P (cglue b) (cglue b')
      (coeq' (f b) (f' b')))^
@' ap (transport (P (coeq (g b))) (cglue b'))
     (cgluel b (f' b'))
@' cgluer (g b) b' = cgluel b (g' b')
        (** Now we just have to rearrange it a bit. *)
        rewrite !concat_pp_p; do 2 apply moveR_Vp; rewrite !concat_p_pp.
H: Funext
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
P: Coeq f g -> Coeq f' g' -> Type
coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a')
cgluel: forall (b : B) (a' : A'),
transport (fun x : Coeq f g => P x (coeq a'))
  (cglue b) (coeq' (f b) a') = 
coeq' (g b) a'
cgluer: forall (a : A) (b' : B'),
transport
  (fun y : Coeq f' g' => P (coeq a) y)
  (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b) 
  (cglue b') (coeq' (f b) (f' b'))
@' ap
     (transport
        (fun x : Coeq f g =>
         P x (coeq (g' b'))) 
        (cglue b)) (cgluer (f b) b')
@' cgluel b (g' b')
b: B
b': B'
ap (transport (P (coeq (g b))) (cglue b'))
  (cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b) (cglue b')
  (coeq' (f b) (f' b'))
@' ap
     (transport
        (fun x : Coeq f g => P x (coeq (g' b')))
        (cglue b)) (cgluer (f b) b')
@' cgluel b (g' b')
        apply cgluelr.
        Close Scope long_path_scope.
  Qed.

End CoeqInd2.

(** ** Symmetry *)

Definition Coeq_sym_map {B A} (f g : B -> A) : Coeq f g -> Coeq g f :=
  Coeq_rec (Coeq g f) coeq (fun b : B => (cglue b)^).

Lemma sect_Coeq_sym_map {B A} {f g : B -> A}
  : (Coeq_sym_map f g) o (Coeq_sym_map g f) == idmap.
B, A: Type
f, g: B -> A
Coeq_sym_map f g o Coeq_sym_map g f == idmap
Proof.
B, A: Type
f, g: B -> A
Coeq_sym_map f g o Coeq_sym_map g f == idmap
  srapply @Coeq_ind.
B, A: Type
f, g: B -> A
forall a : A,
(fun w : Coeq g f =>
 (Coeq_sym_map f g o Coeq_sym_map g f) w = idmap w)
  (coeq a)
B, A: Type
f, g: B -> A
forall b : B,
transport
  (fun w : Coeq g f =>
   (Coeq_sym_map f g o Coeq_sym_map g f) w = idmap w)
  (cglue b) (?coeq' (g b)) = ?coeq' (f b)
  -
B, A: Type
f, g: B -> A
forall a : A,
(fun w : Coeq g f =>
 (Coeq_sym_map f g o Coeq_sym_map g f) w = idmap w)
  (coeq a) reflexivity.
  -
B, A: Type
f, g: B -> A
forall b : B,
transport
  (fun w : Coeq g f =>
   (Coeq_sym_map f g o Coeq_sym_map g f) w = idmap w)
  (cglue b) ((fun a : A => 1) (g b)) =
(fun a : A => 1) (f b) intro b.
B, A: Type
f, g: B -> A
b: B
transport
  (fun w : Coeq g f =>
   (Coeq_sym_map f g o Coeq_sym_map g f) w = idmap w)
  (cglue b) ((fun a : A => 1) (g b)) =
(fun a : A => 1) (f b)
    simpl.
B, A: Type
f, g: B -> A
b: B
transport
  (fun w : Coeq g f =>
   Coeq_sym_map f g (Coeq_sym_map g f w) = w)
  (cglue b) 1 = 1
    abstract (rewrite transport_paths_FFlr, Coeq_rec_beta_cglue, ap_V, Coeq_rec_beta_cglue; hott_simpl).
Defined.

Lemma Coeq_sym {B A} {f g : B -> A} : @Coeq B A f g <~> Coeq g f.
B, A: Type
f, g: B -> A
Coeq f g <~> Coeq g f
Proof.
B, A: Type
f, g: B -> A
Coeq f g <~> Coeq g f
  exact (equiv_adjointify (Coeq_sym_map f g) (Coeq_sym_map g f) sect_Coeq_sym_map sect_Coeq_sym_map).
Defined.

(** ** Descent *)

(** We study "equifibrant" type families over a parallel pair [f, g: B -> A].  By univalence, the descent property tells us that these type families correspond to type families over the coequalizer, and we obtain an induction principle for such type families.  Dependent descent data over some particular descent data are "equifibrant" type families over this descent data.  The "equifibrancy" is only taken over the parallel pair [f g : B -> A], but there is an extra level of dependency coming from the descent data.  In this case, we obtain an induction and recursion principle, but only with a computation rule for the recursion principle.

The theory of descent is interesting to consider in itself.  However, we will use it as a means to structure the code, and to obtain induction and recursion principles that are valuable in proving the flattening lemma, and characterizing path spaces.  Thus we will gloss over the bigger picture, and not consider equivalences of descent data, nor homotopies of their sections.  We will also not elaborate on uniqueness of the induced families.

It's possible to prove the results in the Descent, Flattening and Paths Sections without univalence, by replacing all equivalences with paths, but in practice these results will be used with equivalences as input, making the form below more convenient.  See https://github.com/HoTT/Coq-HoTT/pull/2147#issuecomment-2521570830 for further information *)

Section Descent.

  Context `{Univalence}.

  (** Descent data over [f g : B -> A] is an "equifibrant" or "cartesian" type family [cd_fam : A -> Type].  This means that if [b : B], then the fibers [cd_fam (f b)] and [cd_fam (g b)] are equivalent, witnessed by [cd_e]. *)
  Record cDescent {A B : Type} {f g : B -> A} := {
    cd_fam (a : A) : Type;
    cd_e (b : B) : cd_fam (f b) <~> cd_fam (g b)
  }.
  Global Arguments cDescent {A B} f g.

  (** Let [A] and [B] be types, with a parallel pair [f g : B -> A]. *)
  Context {A B : Type} {f g : B -> A}.

  (** Descent data induces a type family over [Coeq f g]. *)
  Definition fam_cdescent (Pe : cDescent f g)
    : Coeq f g -> Type.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Coeq f g -> Type
  Proof.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Coeq f g -> Type
    snapply (Coeq_rec _ (cd_fam Pe)).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
forall b : B, cd_fam Pe (f b) = cd_fam Pe (g b)
    intro b.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
cd_fam Pe (f b) = cd_fam Pe (g b)
    exact (path_universe_uncurried (cd_e Pe b)).
  Defined.

  (** A type family over [Coeq f g] induces descent data. *)
  Definition cdescent_fam (P : Coeq f g -> Type) : cDescent f g.
H: Univalence
A, B: Type
f, g: B -> A
P: Coeq f g -> Type
cDescent f g
  Proof.
H: Univalence
A, B: Type
f, g: B -> A
P: Coeq f g -> Type
cDescent f g
    snapply Build_cDescent.
H: Univalence
A, B: Type
f, g: B -> A
P: Coeq f g -> Type
A -> Type
H: Univalence
A, B: Type
f, g: B -> A
P: Coeq f g -> Type
forall b : B, ?cd_fam (f b) <~> ?cd_fam (g b)
    -
H: Univalence
A, B: Type
f, g: B -> A
P: Coeq f g -> Type
A -> Type exact (P o coeq).
    -
H: Univalence
A, B: Type
f, g: B -> A
P: Coeq f g -> Type
forall b : B, (P o coeq) (f b) <~> (P o coeq) (g b) intro b.
H: Univalence
A, B: Type
f, g: B -> A
P: Coeq f g -> Type
b: B
(P o coeq) (f b) <~> (P o coeq) (g b)
      exact (equiv_transport P (cglue b)).
  Defined.

  (** Transporting over [fam_cdescent] along [cglue b] is given by [cd_e]. *)
  Definition transport_fam_cdescent_cglue
    (Pe : cDescent f g) (b : B) (pf : cd_fam Pe (f b))
    : transport (fam_cdescent Pe) (cglue b) pf = cd_e Pe b pf.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
transport (fam_cdescent Pe) (cglue b) pf =
cd_e Pe b pf
  Proof.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
transport (fam_cdescent Pe) (cglue b) pf =
cd_e Pe b pf
    napply transport_path_universe'.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
ap (fam_cdescent Pe) (cglue b) =
path_universe (cd_e Pe b)
    napply Coeq_rec_beta_cglue.
  Defined.

  (** A section on the descent data is a fiberwise section that respects the equivalences. *)
  Record cDescentSection {Pe : cDescent f g} := {
    cds_sect (a : A) : cd_fam Pe a;
    cds_e (b : B) : cd_e Pe b (cds_sect (f b)) = cds_sect (g b)
  }.

  Global Arguments cDescentSection Pe : clear implicits.

  (** A descent section induces a genuine section of [fam_cdescent Pe]. *)
  Definition cdescent_ind {Pe : cDescent f g}
    (s : cDescentSection Pe)
    : forall (x : Coeq f g), fam_cdescent Pe x.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
s: cDescentSection Pe
forall x : Coeq f g, fam_cdescent Pe x
  Proof.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
s: cDescentSection Pe
forall x : Coeq f g, fam_cdescent Pe x
    snapply (Coeq_ind _ (cds_sect s)).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
s: cDescentSection Pe
forall b : B,
transport (fam_cdescent Pe) (cglue b)
  (cds_sect s (f b)) = cds_sect s (g b)
    intro b.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
s: cDescentSection Pe
b: B
transport (fam_cdescent Pe) (cglue b)
  (cds_sect s (f b)) = cds_sect s (g b)
    exact (transport_fam_cdescent_cglue Pe b _ @ cds_e s b).
  Defined.

  (** We record its computation rule *)
  Definition cdescent_ind_beta_cglue {Pe : cDescent f g}
    (s : cDescentSection Pe) (b : B)
    : apD (cdescent_ind s) (cglue b) = transport_fam_cdescent_cglue Pe b _ @ cds_e s b
    := Coeq_ind_beta_cglue _ (cds_sect s) _ _.

  (** Dependent descent data over descent data [Pe : cDescent f g] consists of a type family [cdd_fam : forall a : A, cd_fam Pe a -> Type] together with coherences [cdd_e b pf]. *)
  Record cDepDescent {Pe : cDescent f g} := {
    cdd_fam (a : A) (pa : cd_fam Pe a) : Type;
    cdd_e (b : B) (pf : cd_fam Pe (f b))
      : cdd_fam (f b) pf <~> cdd_fam (g b) (cd_e Pe b pf)
  }.

  Global Arguments cDepDescent Pe : clear implicits.

  (** A dependent type family over [fam_cdescent Pe] induces dependent descent data over [Pe]. *)
  Definition cdepdescent_fam {Pe : cDescent f g}
    (Q : forall x : Coeq f g, (fam_cdescent Pe) x -> Type)
    : cDepDescent Pe.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: forall x : Coeq f g, fam_cdescent Pe x -> Type
cDepDescent Pe
  Proof.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: forall x : Coeq f g, fam_cdescent Pe x -> Type
cDepDescent Pe
    snapply Build_cDepDescent.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: forall x : Coeq f g, fam_cdescent Pe x -> Type
forall a : A, cd_fam Pe a -> Type
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: forall x : Coeq f g, fam_cdescent Pe x -> Type
forall (b : B) (pf : cd_fam Pe (f b)),
?cdd_fam (f b) pf <~> ?cdd_fam (g b) (cd_e Pe b pf)
    -
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: forall x : Coeq f g, fam_cdescent Pe x -> Type
forall a : A, cd_fam Pe a -> Type intro a; cbn.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: forall x : Coeq f g, fam_cdescent Pe x -> Type
a: A
cd_fam Pe a -> Type
      exact (Q (coeq a)).
    -
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: forall x : Coeq f g, fam_cdescent Pe x -> Type
forall (b : B) (pf : cd_fam Pe (f b)),
(fun a : A => Q (coeq a) : cd_fam Pe a -> Type) (f b)
  pf <~>
(fun a : A => Q (coeq a) : cd_fam Pe a -> Type) (g b)
  (cd_e Pe b pf) intros b pf.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: forall x : Coeq f g, fam_cdescent Pe x -> Type
b: B
pf: cd_fam Pe (f b)
(fun a : A => Q (coeq a) : cd_fam Pe a -> Type) (f b)
  pf <~>
(fun a : A => Q (coeq a) : cd_fam Pe a -> Type) (g b)
  (cd_e Pe b pf)
      exact (equiv_transportDD (fam_cdescent Pe) Q
               (cglue b) (transport_fam_cdescent_cglue Pe b pf)).
  Defined.

  (** Dependent descent data over [Pe] induces a dependent type family over [fam_cdescent Pe]. *)
  Definition fam_cdepdescent {Pe : cDescent f g} (Qe : cDepDescent Pe)
    : forall (x : Coeq f g), (fam_cdescent Pe x) -> Type.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Qe: cDepDescent Pe
forall x : Coeq f g, fam_cdescent Pe x -> Type
  Proof.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Qe: cDepDescent Pe
forall x : Coeq f g, fam_cdescent Pe x -> Type
    snapply Coeq_ind.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Qe: cDepDescent Pe
forall a : A,
(fun w : Coeq f g => fam_cdescent Pe w -> Type)
  (coeq a)
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Qe: cDepDescent Pe
forall b : B,
transport
  (fun w : Coeq f g => fam_cdescent Pe w -> Type)
  (cglue b) (?coeq' (f b)) = ?coeq' (g b)
    -
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Qe: cDepDescent Pe
forall a : A,
(fun w : Coeq f g => fam_cdescent Pe w -> Type)
  (coeq a) exact (cdd_fam Qe).
    -
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Qe: cDepDescent Pe
forall b : B,
transport
  (fun w : Coeq f g => fam_cdescent Pe w -> Type)
  (cglue b) (cdd_fam Qe (f b)) = cdd_fam Qe (g b) intro b.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Qe: cDepDescent Pe
b: B
transport
  (fun w : Coeq f g => fam_cdescent Pe w -> Type)
  (cglue b) (cdd_fam Qe (f b)) = cdd_fam Qe (g b)
      napply (moveR_transport_p _ (cglue b)).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Qe: cDepDescent Pe
b: B
cdd_fam Qe (f b) =
transport
  (fun w : Coeq f g => fam_cdescent Pe w -> Type)
  (cglue b)^ (cdd_fam Qe (g b))
      funext pa.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Qe: cDepDescent Pe
b: B
pa: fam_cdescent Pe (coeq (f b))
cdd_fam Qe (f b) pa =
transport
  (fun w : Coeq f g => fam_cdescent Pe w -> Type)
  (cglue b)^ (cdd_fam Qe (g b)) pa
      rhs napply transport_arrow_toconst.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Qe: cDepDescent Pe
b: B
pa: fam_cdescent Pe (coeq (f b))
cdd_fam Qe (f b) pa =
cdd_fam Qe (g b)
  (transport (fam_cdescent Pe) ((cglue b)^)^ pa)
      rhs nrefine (ap (cdd_fam _ _) _).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Qe: cDepDescent Pe
b: B
pa: fam_cdescent Pe (coeq (f b))
cdd_fam Qe (f b) pa = cdd_fam Qe (g b) ?Goal
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Qe: cDepDescent Pe
b: B
pa: fam_cdescent Pe (coeq (f b))
transport (fam_cdescent Pe) ((cglue b)^)^ pa = ?Goal
      +
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Qe: cDepDescent Pe
b: B
pa: fam_cdescent Pe (coeq (f b))
cdd_fam Qe (f b) pa = cdd_fam Qe (g b) ?Goal exact (path_universe (cdd_e _ _ _)).
      +
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Qe: cDepDescent Pe
b: B
pa: fam_cdescent Pe (coeq (f b))
transport (fam_cdescent Pe) ((cglue b)^)^ pa =
cd_e Pe b pa lhs napply (ap (fun x => (transport _ x _)) (inv_V (cglue _))).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Qe: cDepDescent Pe
b: B
pa: fam_cdescent Pe (coeq (f b))
transport (fam_cdescent Pe) (cglue b) pa =
cd_e Pe b pa
        exact (transport_fam_cdescent_cglue _ _ _).
  Defined.

  (** A section of dependent descent data [Qe : cDepDescent Pe] is a fiberwise section [cdds_sect], together with coherences [cdds_e]. *)
  Record cDepDescentSection {Pe : cDescent f g} {Qe : cDepDescent Pe} := {
    cdds_sect (a : A) (pa : cd_fam Pe a) : cdd_fam Qe a pa;
    cdds_e (b : B) (pf : cd_fam Pe (f b))
      : cdd_e Qe b pf (cdds_sect (f b) pf) = cdds_sect (g b) (cd_e Pe b pf)
  }.

  Global Arguments cDepDescentSection {Pe} Qe.

  (** A dependent descent section induces a genuine section over the total space of [fam_cdescent Pe]. *)
  Definition cdepdescent_ind {Pe : cDescent f g}
    {Q : forall (x : Coeq f g), (fam_cdescent Pe) x -> Type}
    (s : cDepDescentSection (cdepdescent_fam Q))
    : forall (x : Coeq f g) (px : fam_cdescent Pe x), Q x px.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: forall x : Coeq f g, fam_cdescent Pe x -> Type
s: cDepDescentSection (cdepdescent_fam Q)
forall (x : Coeq f g) (px : fam_cdescent Pe x), Q x px
    Proof.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: forall x : Coeq f g, fam_cdescent Pe x -> Type
s: cDepDescentSection (cdepdescent_fam Q)
forall (x : Coeq f g) (px : fam_cdescent Pe x), Q x px
      napply (Coeq_ind _ (cdds_sect s) _).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: forall x : Coeq f g, fam_cdescent Pe x -> Type
s: cDepDescentSection (cdepdescent_fam Q)
forall b : B,
transport
  (fun w : Coeq f g =>
   forall px : fam_cdescent Pe w, Q w px) (cglue b)
  (cdds_sect s (f b)) = cdds_sect s (g b)
      intro b.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: forall x : Coeq f g, fam_cdescent Pe x -> Type
s: cDepDescentSection (cdepdescent_fam Q)
b: B
transport
  (fun w : Coeq f g =>
   forall px : fam_cdescent Pe w, Q w px) (cglue b)
  (cdds_sect s (f b)) = cdds_sect s (g b)
      apply dpath_forall.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: forall x : Coeq f g, fam_cdescent Pe x -> Type
s: cDepDescentSection (cdepdescent_fam Q)
b: B
forall y1 : fam_cdescent Pe (coeq (f b)),
transportD (fam_cdescent Pe) Q (cglue b) y1
  (cdds_sect s (f b) y1) =
cdds_sect s (g b)
  (transport (fam_cdescent Pe) (cglue b) y1)
      intro pf.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: forall x : Coeq f g, fam_cdescent Pe x -> Type
s: cDepDescentSection (cdepdescent_fam Q)
b: B
pf: fam_cdescent Pe (coeq (f b))
transportD (fam_cdescent Pe) Q (cglue b) pf
  (cdds_sect s (f b) pf) =
cdds_sect s (g b)
  (transport (fam_cdescent Pe) (cglue b) pf)
      apply (equiv_inj (transport (Q (coeq (g b))) (transport_fam_cdescent_cglue Pe b pf))).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: forall x : Coeq f g, fam_cdescent Pe x -> Type
s: cDepDescentSection (cdepdescent_fam Q)
b: B
pf: fam_cdescent Pe (coeq (f b))
transport (Q (coeq (g b)))
  (transport_fam_cdescent_cglue Pe b pf)
  (transportD (fam_cdescent Pe) Q (cglue b) pf
     (cdds_sect s (f b) pf)) =
transport (Q (coeq (g b)))
  (transport_fam_cdescent_cglue Pe b pf)
  (cdds_sect s (g b)
     (transport (fam_cdescent Pe) (cglue b) pf))
      rhs exact (apD (cdds_sect s (g b)) (transport_fam_cdescent_cglue Pe b pf)).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: forall x : Coeq f g, fam_cdescent Pe x -> Type
s: cDepDescentSection (cdepdescent_fam Q)
b: B
pf: fam_cdescent Pe (coeq (f b))
transport (Q (coeq (g b)))
  (transport_fam_cdescent_cglue Pe b pf)
  (transportD (fam_cdescent Pe) Q (cglue b) pf
     (cdds_sect s (f b) pf)) =
cdds_sect s (g b) (cd_e Pe b pf)
      exact (cdds_e s b pf).
    Defined.

  (** The data for a section into a constant type family. *)
  Record cDepDescentConstSection {Pe : cDescent f g} {Q : Type} := {
    cddcs_sect (a : A) (pa : cd_fam Pe a) : Q;
    cddcs_e (b : B) (pf : cd_fam Pe (f b))
      : cddcs_sect (f b) pf = cddcs_sect (g b) (cd_e Pe b pf)
  }.

  Global Arguments cDepDescentConstSection Pe Q : clear implicits.

  (** The data for a section of a constant family induces a section over the total space of [fam_cdescent Pe]. *)
  Definition cdepdescent_rec {Pe : cDescent f g} {Q : Type}
    (s : cDepDescentConstSection Pe Q)
    : forall (x : Coeq f g), fam_cdescent Pe x -> Q.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
forall x : Coeq f g, fam_cdescent Pe x -> Q
  Proof.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
forall x : Coeq f g, fam_cdescent Pe x -> Q
    snapply (Coeq_ind _ (cddcs_sect s)).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
forall b : B,
transport (fun w : Coeq f g => fam_cdescent Pe w -> Q)
  (cglue b) (cddcs_sect s (f b)) = cddcs_sect s (g b)
    intro b.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
transport (fun w : Coeq f g => fam_cdescent Pe w -> Q)
  (cglue b) (cddcs_sect s (f b)) = cddcs_sect s (g b)
    napply dpath_arrow.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
forall y1 : fam_cdescent Pe (coeq (f b)),
transport (fun _ : Coeq f g => Q) (cglue b)
  (cddcs_sect s (f b) y1) =
cddcs_sect s (g b)
  (transport (fam_cdescent Pe) (cglue b) y1)
    intro pf.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: fam_cdescent Pe (coeq (f b))
transport (fun _ : Coeq f g => Q) (cglue b)
  (cddcs_sect s (f b) pf) =
cddcs_sect s (g b)
  (transport (fam_cdescent Pe) (cglue b) pf)
    lhs napply transport_const.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: fam_cdescent Pe (coeq (f b))
cddcs_sect s (f b) pf =
cddcs_sect s (g b)
  (transport (fam_cdescent Pe) (cglue b) pf)
    rhs napply (ap _ (transport_fam_cdescent_cglue Pe b pf)).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: fam_cdescent Pe (coeq (f b))
cddcs_sect s (f b) pf =
cddcs_sect s (g b) (cd_e Pe b pf)
    exact (cddcs_e s b pf).
  Defined.

  (** Here is the computation rule on paths. *)
  Definition cdepdescent_rec_beta_cglue {Pe : cDescent f g} {Q : Type}
    (s : cDepDescentConstSection Pe Q)
    (b : B) {pf : cd_fam Pe (f b)} {pg : cd_fam Pe (g b)} (pb : cd_e Pe b pf = pg)
    : ap (sig_rec (cdepdescent_rec s)) (path_sigma _ (coeq (f b); pf) (coeq (g b); pg) (cglue b) (transport_fam_cdescent_cglue Pe b pf @ pb))
      = cddcs_e s b pf @ ap (cddcs_sect s (g b)) pb.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
pg: cd_fam Pe (g b)
pb: cd_e Pe b pf = pg
ap (sig_rec (cdepdescent_rec s))
  (path_sigma (fam_cdescent Pe) (coeq (f b); pf)
     (coeq (g b); pg) (cglue b)
     (transport_fam_cdescent_cglue Pe b pf @ pb)) =
cddcs_e s b pf @ ap (cddcs_sect s (g b)) pb
  Proof.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
pg: cd_fam Pe (g b)
pb: cd_e Pe b pf = pg
ap (sig_rec (cdepdescent_rec s))
  (path_sigma (fam_cdescent Pe) (coeq (f b); pf)
     (coeq (g b); pg) (cglue b)
     (transport_fam_cdescent_cglue Pe b pf @ pb)) =
cddcs_e s b pf @ ap (cddcs_sect s (g b)) pb
    Open Scope long_path_scope.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
pg: cd_fam Pe (g b)
pb: cd_e Pe b pf = pg
ap (sig_rec (cdepdescent_rec s))
  (path_sigma (fam_cdescent Pe) (coeq (f b); pf)
     (coeq (g b); pg) (cglue b)
     (transport_fam_cdescent_cglue Pe b pf
      @' pb)) =
cddcs_e s b pf
@' ap (cddcs_sect s (g b)) pb
    destruct pb.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
ap (sig_rec (cdepdescent_rec s))
  (path_sigma (fam_cdescent Pe) (coeq (f b); pf)
     (coeq (g b); cd_e Pe b pf) (cglue b)
     (transport_fam_cdescent_cglue Pe b pf
      @' 1)) =
cddcs_e s b pf
@' ap (cddcs_sect s (g b)) 1
    rhs napply concat_p1.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
ap (sig_rec (cdepdescent_rec s))
  (path_sigma (fam_cdescent Pe) (coeq (f b); pf)
     (coeq (g b); cd_e Pe b pf) (cglue b)
     (transport_fam_cdescent_cglue Pe b pf
      @' 1)) = cddcs_e s b pf
    lhs napply ap_sig_rec_path_sigma.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
(transport_const (cglue b)
   (cdepdescent_rec s (coeq (f b)) pf))^
@' (ap
      (fun x : fam_cdescent Pe (coeq (f b)) =>
       transport (fun _ : Coeq f g => Q) (cglue b)
         (cdepdescent_rec s (coeq (f b)) x))
      (transport_Vp (fam_cdescent Pe) (cglue b) pf))^
@' (transport_arrow (cglue b)
      (cdepdescent_rec s (coeq (f b)))
      (transport (fam_cdescent Pe) (cglue b) pf))^
@' ap10 (apD (cdepdescent_rec s) (cglue b))
     (transport (fam_cdescent Pe) (cglue b) pf)
@' ap (cdepdescent_rec s (coeq (g b)))
     (transport_fam_cdescent_cglue Pe b pf
      @' 1) = cddcs_e s b pf
    lhs napply (ap (fun x => _ (ap10 x _) @ _)).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
apD (cdepdescent_rec s) (cglue b) = ?Goal
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
(transport_const (cglue b)
   (cdepdescent_rec s (coeq (f b)) pf))^
@' (ap
      (fun x : fam_cdescent Pe (coeq (f b)) =>
       transport (fun _ : Coeq f g => Q) (cglue b)
         (cdepdescent_rec s (coeq (f b)) x))
      (transport_Vp (fam_cdescent Pe) (cglue b) pf))^
@' (transport_arrow (cglue b)
      (cdepdescent_rec s (coeq (f b)))
      (transport (fam_cdescent Pe) (cglue b) pf))^
@' ap10 ?Goal
     (transport (fam_cdescent Pe) (cglue b) pf)
@' ap (cdepdescent_rec s (coeq (g b)))
     (transport_fam_cdescent_cglue Pe b pf
      @' 1) = cddcs_e s b pf
    1: napply Coeq_ind_beta_cglue.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
(transport_const (cglue b)
   (cdepdescent_rec s (coeq (f b)) pf))^
@' (ap
      (fun x : fam_cdescent Pe (coeq (f b)) =>
       transport (fun _ : Coeq f g => Q) (cglue b)
         (cdepdescent_rec s (coeq (f b)) x))
      (transport_Vp (fam_cdescent Pe) (cglue b) pf))^
@' (transport_arrow (cglue b)
      (cdepdescent_rec s (coeq (f b)))
      (transport (fam_cdescent Pe) (cglue b) pf))^
@' ap10
     (dpath_arrow (fam_cdescent Pe)
        (fun _ : Coeq f g => Q) (cglue b)
        (cddcs_sect s (f b)) (cddcs_sect s (g b))
        (fun pf : fam_cdescent Pe (coeq (f b)) =>
         transport_const (cglue b)
           (cddcs_sect s (f b) pf)
         @' (cddcs_e s b pf
             @' (ap (cddcs_sect s (g b))
                   (transport_fam_cdescent_cglue Pe b
                      pf))^)))
     (transport (fam_cdescent Pe) (cglue b) pf)
@' ap (cdepdescent_rec s (coeq (g b)))
     (transport_fam_cdescent_cglue Pe b pf
      @' 1) = cddcs_e s b pf
    do 3 lhs napply concat_pp_p.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
(transport_const (cglue b)
   (cdepdescent_rec s (coeq (f b)) pf))^
@' ((ap
       (fun x : fam_cdescent Pe (coeq (f b)) =>
        transport (fun _ : Coeq f g => Q) (cglue b)
          (cdepdescent_rec s (coeq (f b)) x))
       (transport_Vp (fam_cdescent Pe) (cglue b) pf))^
    @' ((transport_arrow (cglue b)
           (cdepdescent_rec s (coeq (f b)))
           (transport (fam_cdescent Pe) (cglue b) pf))^
        @' (ap10
              (dpath_arrow (fam_cdescent Pe)
                 (fun _ : Coeq f g => Q) (cglue b)
                 (cddcs_sect s (f b))
                 (cddcs_sect s (g b))
                 (fun
                    pf : fam_cdescent Pe (coeq (f b))
                  =>
                  transport_const (cglue b)
                    (cddcs_sect s (f b) pf)
                  @' (cddcs_e s b pf
                      @' (ap (cddcs_sect s (g b))
                            (transport_fam_cdescent_cglue
                               Pe b pf))^)))
              (transport (fam_cdescent Pe) (cglue b)
                 pf)
            @' ap (cdepdescent_rec s (coeq (g b)))
                 (transport_fam_cdescent_cglue Pe b pf
                  @' 1)))) = cddcs_e s b pf
    apply moveR_Vp.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
(ap
   (fun x : fam_cdescent Pe (coeq (f b)) =>
    transport (fun _ : Coeq f g => Q) (cglue b)
      (cdepdescent_rec s (coeq (f b)) x))
   (transport_Vp (fam_cdescent Pe) (cglue b) pf))^
@' ((transport_arrow (cglue b)
       (cdepdescent_rec s (coeq (f b)))
       (transport (fam_cdescent Pe) (cglue b) pf))^
    @' (ap10
          (dpath_arrow (fam_cdescent Pe)
             (fun _ : Coeq f g => Q) (cglue b)
             (cddcs_sect s (f b)) (cddcs_sect s (g b))
             (fun pf : fam_cdescent Pe (coeq (f b)) =>
              transport_const (cglue b)
                (cddcs_sect s (f b) pf)
              @' (cddcs_e s b pf
                  @' (ap (cddcs_sect s (g b))
                        (transport_fam_cdescent_cglue
                           Pe b pf))^)))
          (transport (fam_cdescent Pe) (cglue b) pf)
        @' ap (cdepdescent_rec s (coeq (g b)))
             (transport_fam_cdescent_cglue Pe b pf
              @' 1))) =
transport_const (cglue b)
  (cdepdescent_rec s (coeq (f b)) pf)
@' cddcs_e s b pf
    lhs nrefine (1 @@ (1 @@ (_ @@ 1))).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
ap10
  (dpath_arrow (fam_cdescent Pe)
     (fun _ : Coeq f g => Q) (cglue b)
     (cddcs_sect s (f b)) (cddcs_sect s (g b))
     (fun pf : fam_cdescent Pe (coeq (f b)) =>
      transport_const (cglue b)
        (cddcs_sect s (f b) pf)
      @' (cddcs_e s b pf
          @' (ap (cddcs_sect s (g b))
                (transport_fam_cdescent_cglue Pe b pf))^)))
  (transport (fam_cdescent Pe) (cglue b) pf) = ?Goal
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
(ap
   (fun x : fam_cdescent Pe (coeq (f b)) =>
    transport (fun _ : Coeq f g => Q) (cglue b)
      (cdepdescent_rec s (coeq (f b)) x))
   (transport_Vp (fam_cdescent Pe) (cglue b) pf))^
@' ((transport_arrow (cglue b)
       (cdepdescent_rec s (coeq (f b)))
       (transport (fam_cdescent Pe) (cglue b) pf))^
    @' (?Goal
        @' ap (cdepdescent_rec s (coeq (g b)))
             (transport_fam_cdescent_cglue Pe b pf
              @' 1))) =
transport_const (cglue b)
  (cdepdescent_rec s (coeq (f b)) pf)
@' cddcs_e s b pf
    1: napply (ap10_dpath_arrow (fam_cdescent Pe) (fun _ => Q) (cglue b)).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
(ap
   (fun x : fam_cdescent Pe (coeq (f b)) =>
    transport (fun _ : Coeq f g => Q) (cglue b)
      (cdepdescent_rec s (coeq (f b)) x))
   (transport_Vp (fam_cdescent Pe) (cglue b) pf))^
@' ((transport_arrow (cglue b)
       (cdepdescent_rec s (coeq (f b)))
       (transport (fam_cdescent Pe) (cglue b) pf))^
    @' (transport_arrow (cglue b)
          (cdepdescent_rec s (coeq (f b)))
          (transport (fam_cdescent Pe) (cglue b) pf)
        @' ap
             (fun x : fam_cdescent Pe (coeq (f b)) =>
              transport (fun _ : Coeq f g => Q)
                (cglue b)
                (cdepdescent_rec s (coeq (f b)) x))
             (transport_Vp (fam_cdescent Pe) (cglue b)
                pf)
        @' (fun pf : fam_cdescent Pe (coeq (f b)) =>
            transport_const (cglue b)
              (cddcs_sect s (f b) pf)
            @' (cddcs_e s b pf
                @' (ap (cddcs_sect s (g b))
                      (transport_fam_cdescent_cglue Pe
                         b pf))^)) pf
        @' ap (cdepdescent_rec s (coeq (g b)))
             (transport_fam_cdescent_cglue Pe b pf
              @' 1))) =
transport_const (cglue b)
  (cdepdescent_rec s (coeq (f b)) pf)
@' cddcs_e s b pf
    lhs nrefine (1 @@ _).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
(transport_arrow (cglue b)
   (cdepdescent_rec s (coeq (f b)))
   (transport (fam_cdescent Pe) (cglue b) pf))^
@' (transport_arrow (cglue b)
      (cdepdescent_rec s (coeq (f b)))
      (transport (fam_cdescent Pe) (cglue b) pf)
    @' ap
         (fun x : fam_cdescent Pe (coeq (f b)) =>
          transport (fun _ : Coeq f g => Q) (cglue b)
            (cdepdescent_rec s (coeq (f b)) x))
         (transport_Vp (fam_cdescent Pe) (cglue b) pf)
    @' (transport_const (cglue b)
          (cddcs_sect s (f b) pf)
        @' (cddcs_e s b pf
            @' (ap (cddcs_sect s (g b))
                  (transport_fam_cdescent_cglue Pe b
                     pf))^))
    @' ap (cdepdescent_rec s (coeq (g b)))
         (transport_fam_cdescent_cglue Pe b pf
          @' 1)) = ?Goal
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
(ap
   (fun x : fam_cdescent Pe (coeq (f b)) =>
    transport (fun _ : Coeq f g => Q) (cglue b)
      (cdepdescent_rec s (coeq (f b)) x))
   (transport_Vp (fam_cdescent Pe) (cglue b) pf))^
@' ?Goal =
transport_const (cglue b)
  (cdepdescent_rec s (coeq (f b)) pf)
@' cddcs_e s b pf
    {
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
(transport_arrow (cglue b)
   (cdepdescent_rec s (coeq (f b)))
   (transport (fam_cdescent Pe) (cglue b) pf))^
@' (transport_arrow (cglue b)
      (cdepdescent_rec s (coeq (f b)))
      (transport (fam_cdescent Pe) (cglue b) pf)
    @' ap
         (fun x : fam_cdescent Pe (coeq (f b)) =>
          transport (fun _ : Coeq f g => Q) (cglue b)
            (cdepdescent_rec s (coeq (f b)) x))
         (transport_Vp (fam_cdescent Pe) (cglue b) pf)
    @' (transport_const (cglue b)
          (cddcs_sect s (f b) pf)
        @' (cddcs_e s b pf
            @' (ap (cddcs_sect s (g b))
                  (transport_fam_cdescent_cglue Pe b
                     pf))^))
    @' ap (cdepdescent_rec s (coeq (g b)))
         (transport_fam_cdescent_cglue Pe b pf
          @' 1)) = ?Goal lhs napply (1 @@ concat_pp_p _ _ _).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
(transport_arrow (cglue b)
   (cdepdescent_rec s (coeq (f b)))
   (transport (fam_cdescent Pe) (cglue b) pf))^
@' (transport_arrow (cglue b)
      (cdepdescent_rec s (coeq (f b)))
      (transport (fam_cdescent Pe) (cglue b) pf)
    @' ap
         (fun x : fam_cdescent Pe (coeq (f b)) =>
          transport (fun _ : Coeq f g => Q) (cglue b)
            (cdepdescent_rec s (coeq (f b)) x))
         (transport_Vp (fam_cdescent Pe) (cglue b) pf)
    @' (transport_const (cglue b)
          (cddcs_sect s (f b) pf)
        @' (cddcs_e s b pf
            @' (ap (cddcs_sect s (g b))
                  (transport_fam_cdescent_cglue Pe b
                     pf))^)
        @' ap (cdepdescent_rec s (coeq (g b)))
             (transport_fam_cdescent_cglue Pe b pf
              @' 1))) = ?Goal
      lhs napply (1 @@ concat_pp_p _ _ _).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
(transport_arrow (cglue b)
   (cdepdescent_rec s (coeq (f b)))
   (transport (fam_cdescent Pe) (cglue b) pf))^
@' (transport_arrow (cglue b)
      (cdepdescent_rec s (coeq (f b)))
      (transport (fam_cdescent Pe) (cglue b) pf)
    @' (ap
          (fun x : fam_cdescent Pe (coeq (f b)) =>
           transport (fun _ : Coeq f g => Q) (cglue b)
             (cdepdescent_rec s (coeq (f b)) x))
          (transport_Vp (fam_cdescent Pe) (cglue b) pf)
        @' (transport_const (cglue b)
              (cddcs_sect s (f b) pf)
            @' (cddcs_e s b pf
                @' (ap (cddcs_sect s (g b))
                      (transport_fam_cdescent_cglue Pe
                         b pf))^)
            @' ap (cdepdescent_rec s (coeq (g b)))
                 (transport_fam_cdescent_cglue Pe b pf
                  @' 1)))) = ?Goal
      lhs napply concat_V_pp.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
ap
  (fun x : fam_cdescent Pe (coeq (f b)) =>
   transport (fun _ : Coeq f g => Q) (cglue b)
     (cdepdescent_rec s (coeq (f b)) x))
  (transport_Vp (fam_cdescent Pe) (cglue b) pf)
@' (transport_const (cglue b) (cddcs_sect s (f b) pf)
    @' (cddcs_e s b pf
        @' (ap (cddcs_sect s (g b))
              (transport_fam_cdescent_cglue Pe b pf))^)
    @' ap (cdepdescent_rec s (coeq (g b)))
         (transport_fam_cdescent_cglue Pe b pf
          @' 1)) = ?Goal
      lhs napply (1 @@ concat_pp_p _ _ _).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
ap
  (fun x : fam_cdescent Pe (coeq (f b)) =>
   transport (fun _ : Coeq f g => Q) (cglue b)
     (cdepdescent_rec s (coeq (f b)) x))
  (transport_Vp (fam_cdescent Pe) (cglue b) pf)
@' (transport_const (cglue b) (cddcs_sect s (f b) pf)
    @' (cddcs_e s b pf
        @' (ap (cddcs_sect s (g b))
              (transport_fam_cdescent_cglue Pe b pf))^
        @' ap (cdepdescent_rec s (coeq (g b)))
             (transport_fam_cdescent_cglue Pe b pf
              @' 1))) = ?Goal
      rewrite concat_p1.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
ap
  (fun x : fam_cdescent Pe (coeq (f b)) =>
   transport (fun _ : Coeq f g => Q) (cglue b)
     (cdepdescent_rec s (coeq (f b)) x))
  (transport_Vp (fam_cdescent Pe) (cglue b) pf)
@' (transport_const (cglue b) (cddcs_sect s (f b) pf)
    @' (cddcs_e s b pf
        @' (ap (cddcs_sect s (g b))
              (transport_fam_cdescent_cglue Pe b pf))^
        @' ap (cdepdescent_rec s (coeq (g b)))
             (transport_fam_cdescent_cglue Pe b pf))) =
?Goal
      exact (1 @@ (1 @@ concat_pV_p _ _)). }
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Q: Type
s: cDepDescentConstSection Pe Q
b: B
pf: cd_fam Pe (f b)
(ap
   (fun x : fam_cdescent Pe (coeq (f b)) =>
    transport (fun _ : Coeq f g => Q) (cglue b)
      (cdepdescent_rec s (coeq (f b)) x))
   (transport_Vp (fam_cdescent Pe) (cglue b) pf))^
@' (ap
      (fun x : fam_cdescent Pe (coeq (f b)) =>
       transport (fun _ : Coeq f g => Q) (cglue b)
         (cdepdescent_rec s (coeq (f b)) x))
      (transport_Vp (fam_cdescent Pe) (cglue b) pf)
    @' (transport_const (cglue b)
          (cddcs_sect s (f b) pf)
        @' cddcs_e s b pf)) =
transport_const (cglue b)
  (cdepdescent_rec s (coeq (f b)) pf)
@' cddcs_e s b pf
    napply concat_V_pp.
    Close Scope long_path_scope.
  Defined.

End Descent.

(** ** The flattening lemma *)

(** We saw above that given descent data [Pe] over a parallel pair [f g : B -> A], we obtained a type family [fam_cdescent Pe] over the coequalizer.  The flattening lemma describes the total space [sig (fam_cdescent Pe)] of this type family as a coequalizer of [sig (cd_fam Pe)] by a certain parallel pair.  This follows from the work above, which shows that [sig (fam_cdescent Pe)] has the same universal property as this coequalizer.

The flattening lemma here also follows from the flattening lemma for [GraphQuotients], avoiding the need for the material in Section Descent.  However, that material is likely useful in general, so we have given an independent proof of the flattening lemma.  See versions of the library before December 5, 2024 for the proof using the flattening lemma for [GraphQuotients]. *)

Section Flattening.

  Context `{Univalence} {A B : Type} {f g : B -> A} (Pe : cDescent f g).

  (** We mimic the constructors of [Coeq] for the total space.  Here is the point constructor, in curried form. *)
  Definition flatten_cd {a : A} (pa : cd_fam Pe a) : sig (fam_cdescent Pe)
    := (coeq a; pa).

  (** And here is the path constructor. *)
  Definition flatten_cd_glue (b : B)
    {pf : cd_fam Pe (f b)} {pg : cd_fam Pe (g b)} (pb : cd_e Pe b pf = pg)
    : flatten_cd pf = flatten_cd pg.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
pg: cd_fam Pe (g b)
pb: cd_e Pe b pf = pg
flatten_cd pf = flatten_cd pg
  Proof.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
pg: cd_fam Pe (g b)
pb: cd_e Pe b pf = pg
flatten_cd pf = flatten_cd pg
    snapply path_sigma.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
pg: cd_fam Pe (g b)
pb: cd_e Pe b pf = pg
(flatten_cd pf).1 = (flatten_cd pg).1
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
pg: cd_fam Pe (g b)
pb: cd_e Pe b pf = pg
transport (fam_cdescent Pe) ?p (flatten_cd pf).2 =
(flatten_cd pg).2
    -
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
pg: cd_fam Pe (g b)
pb: cd_e Pe b pf = pg
(flatten_cd pf).1 = (flatten_cd pg).1 by apply cglue.
    -
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
pg: cd_fam Pe (g b)
pb: cd_e Pe b pf = pg
transport (fam_cdescent Pe) (cglue b)
  (flatten_cd pf).2 = (flatten_cd pg).2 lhs napply transport_fam_cdescent_cglue.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
pg: cd_fam Pe (g b)
pb: cd_e Pe b pf = pg
cd_e Pe b (flatten_cd pf).2 = (flatten_cd pg).2
      exact pb.
  Defined.

  (** Now that we've shown that [fam_cdescent Pe] acts like a [Coeq] of [sig (cd_fam Pe)] by an appropriate parallel pair, we can use this to prove the flattening lemma.  The maps back and forth are very easy so this could almost be a formal consequence of the induction principle. *)
  Lemma equiv_cd_flatten : sig (fam_cdescent Pe) <~>
    Coeq (functor_sigma f (fun _ => idmap)) (functor_sigma g (cd_e Pe)).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
{x : _ & fam_cdescent Pe x} <~>
Coeq (functor_sigma f (fun a : B => idmap))
  (functor_sigma g (fun b : B => cd_e Pe b))
  Proof.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
{x : _ & fam_cdescent Pe x} <~>
Coeq (functor_sigma f (fun a : B => idmap))
  (functor_sigma g (fun b : B => cd_e Pe b))
    snapply equiv_adjointify.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
{x : _ & fam_cdescent Pe x} ->
Coeq (functor_sigma f (fun a : B => idmap))
  (functor_sigma g (fun b : B => cd_e Pe b))
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Coeq (functor_sigma f (fun a : B => idmap))
  (functor_sigma g (fun b : B => cd_e Pe b)) ->
{x : _ & fam_cdescent Pe x}
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
?f o ?g == idmap
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
?g o ?f == idmap
    -
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
{x : _ & fam_cdescent Pe x} ->
Coeq (functor_sigma f (fun a : B => idmap))
  (functor_sigma g (fun b : B => cd_e Pe b)) snapply sig_rec.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
forall proj1 : Coeq f g,
fam_cdescent Pe proj1 ->
Coeq (functor_sigma f (fun a : B => idmap))
  (functor_sigma g (fun b : B => cd_e Pe b))
      snapply cdepdescent_rec.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
cDepDescentConstSection Pe
  (Coeq (functor_sigma f (fun a : B => idmap))
     (functor_sigma g (fun b : B => cd_e Pe b)))
      snapply Build_cDepDescentConstSection.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
forall a : A,
cd_fam Pe a ->
Coeq (functor_sigma f (fun a0 : B => idmap))
  (functor_sigma g (fun b : B => cd_e Pe b))
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
forall (b : B) (pf : cd_fam Pe (f b)),
?cddcs_sect (f b) pf =
?cddcs_sect (g b) (cd_e Pe b pf)
      +
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
forall a : A,
cd_fam Pe a ->
Coeq (functor_sigma f (fun a0 : B => idmap))
  (functor_sigma g (fun b : B => cd_e Pe b)) exact (fun a x => coeq (a; x)).
      +
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
forall (b : B) (pf : cd_fam Pe (f b)),
(fun (a : A) (x : cd_fam Pe a) => coeq (a; x)) (f b)
  pf =
(fun (a : A) (x : cd_fam Pe a) => coeq (a; x)) (g b)
  (cd_e Pe b pf) intros b pf.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
(fun (a : A) (x : cd_fam Pe a) => coeq (a; x)) (f b)
  pf =
(fun (a : A) (x : cd_fam Pe a) => coeq (a; x)) (g b)
  (cd_e Pe b pf)
      cbn.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
coeq (f b; pf) = coeq (g b; cd_e Pe b pf)
      exact (@cglue _ _
        (functor_sigma f (fun _ => idmap)) (functor_sigma g (cd_e Pe)) (b; pf)).
    -
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Coeq (functor_sigma f (fun a : B => idmap))
  (functor_sigma g (fun b : B => cd_e Pe b)) ->
{x : _ & fam_cdescent Pe x} snapply Coeq_rec.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
{x : _ & cd_fam Pe x} -> {x : _ & fam_cdescent Pe x}
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
forall b : {H : B & cd_fam Pe (f H)},
?coeq' (functor_sigma f (fun a : B => idmap) b) =
?coeq' (functor_sigma g (fun b0 : B => cd_e Pe b0) b)
      +
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
{x : _ & cd_fam Pe x} -> {x : _ & fam_cdescent Pe x} exact (fun '(a; x) => (coeq a; x)).
      +
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
forall b : {H : B & cd_fam Pe (f H)},
(fun pat : {x : _ & cd_fam Pe x} =>
 let x := pat in
 let a := x.1 in let x0 := x.2 in (coeq a; x0))
  (functor_sigma f (fun a : B => idmap) b) =
(fun pat : {x : _ & cd_fam Pe x} =>
 let x := pat in
 let a := x.1 in let x0 := x.2 in (coeq a; x0))
  (functor_sigma g (fun b0 : B => cd_e Pe b0) b) intros [b pf]; cbn.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
(coeq (f b); pf) = (coeq (g b); cd_e Pe b pf)
        exact (flatten_cd_glue b 1).
    -
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
sig_rec
  (cdepdescent_rec
     {|
       cddcs_sect :=
         fun (a : A) (x : cd_fam Pe a) => coeq (a; x);
       cddcs_e :=
         fun (b : B) (pf : cd_fam Pe (f b)) =>
         cglue (b; pf)
         :
         (fun (a : A) (x : cd_fam Pe a) => coeq (a; x))
           (f b) pf =
         (fun (a : A) (x : cd_fam Pe a) => coeq (a; x))
           (g b) (cd_e Pe b pf)
     |})
o Coeq_rec {x : _ & fam_cdescent Pe x}
    (fun pat : {x : _ & cd_fam Pe x} =>
     let x := pat in
     let a := x.1 in let x0 := x.2 in (coeq a; x0))
    (fun b0 : {H : B & cd_fam Pe (f H)} =>
     (fun (b : B) (pf : cd_fam Pe (f b)) =>
      flatten_cd_glue b 1
      :
      (let x :=
         functor_sigma f (fun a : B => idmap) (b; pf)
         in
       let a := x.1 in let x0 := x.2 in (coeq a; x0)) =
      (let x :=
         functor_sigma g (fun b1 : B => cd_e Pe b1)
           (b; pf) in
       let a := x.1 in let x0 := x.2 in (coeq a; x0)))
       b0.1 b0.2) == idmap snapply Coeq_ind; cbn beta.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
forall a : {x : _ & cd_fam Pe x},
sig_rec
  (cdepdescent_rec
     {|
       cddcs_sect :=
         fun (a0 : A) (x : cd_fam Pe a0) =>
         coeq (a0; x);
       cddcs_e :=
         fun (b : B) (pf : cd_fam Pe (f b)) =>
         cglue (b; pf)
     |})
  (Coeq_rec {x : _ & fam_cdescent Pe x}
     (fun pat : {x : _ & cd_fam Pe x} =>
      let x := pat in
      let a0 := x.1 in let x0 := x.2 in (coeq a0; x0))
     (fun b0 : {H : B & cd_fam Pe (f H)} =>
      flatten_cd_glue b0.1 1) (coeq a)) = coeq a
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
forall b : {H : B & cd_fam Pe (f H)},
transport
  (fun
     w : Coeq (functor_sigma f (fun a : B => idmap))
           (functor_sigma g (fun b0 : B => cd_e Pe b0))
   =>
   sig_rec
     (cdepdescent_rec
        {|
          cddcs_sect :=
            fun (a : A) (x : cd_fam Pe a) =>
            coeq (a; x);
          cddcs_e :=
            fun (b0 : B) (pf : cd_fam Pe (f b0)) =>
            cglue (b0; pf)
        |})
     (Coeq_rec {x : _ & fam_cdescent Pe x}
        (fun pat : {x : _ & cd_fam Pe x} =>
         let x := pat in
         let a := x.1 in let x0 := x.2 in (coeq a; x0))
        (fun b0 : {H : B & cd_fam Pe (f H)} =>
         flatten_cd_glue b0.1 1) w) = w) (cglue b)
  (?Goal (functor_sigma f (fun a : B => idmap) b)) =
?Goal (functor_sigma g (fun b0 : B => cd_e Pe b0) b)
      1: reflexivity.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
forall b : {H : B & cd_fam Pe (f H)},
transport
  (fun
     w : Coeq (functor_sigma f (fun a : B => idmap))
           (functor_sigma g (fun b0 : B => cd_e Pe b0))
   =>
   sig_rec
     (cdepdescent_rec
        {|
          cddcs_sect :=
            fun (a : A) (x : cd_fam Pe a) =>
            coeq (a; x);
          cddcs_e :=
            fun (b0 : B) (pf : cd_fam Pe (f b0)) =>
            cglue (b0; pf)
        |})
     (Coeq_rec {x : _ & fam_cdescent Pe x}
        (fun pat : {x : _ & cd_fam Pe x} =>
         let x := pat in
         let a := x.1 in let x0 := x.2 in (coeq a; x0))
        (fun b0 : {H : B & cd_fam Pe (f H)} =>
         flatten_cd_glue b0.1 1) w) = w) (cglue b)
  ((fun a : {x : _ & cd_fam Pe x} => 1)
     (functor_sigma f (fun a : B => idmap) b)) =
(fun a : {x : _ & cd_fam Pe x} => 1)
  (functor_sigma g (fun b0 : B => cd_e Pe b0) b)
      intros [b pf]; cbn.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
transport
  (fun
     w : Coeq (functor_sigma f (fun a : B => idmap))
           (functor_sigma g (fun b : B => cd_e Pe b))
   =>
   sig_rec
     (cdepdescent_rec
        {|
          cddcs_sect :=
            fun (a : A) (x : cd_fam Pe a) =>
            coeq (a; x);
          cddcs_e :=
            fun (b : B) (pf : cd_fam Pe (f b)) =>
            cglue (b; pf)
        |})
     (Coeq_rec {x : _ & fam_cdescent Pe x}
        (fun pat : {x : _ & cd_fam Pe x} =>
         (coeq pat.1; pat.2))
        (fun b0 : {H : B & cd_fam Pe (f H)} =>
         flatten_cd_glue b0.1 1) w) = w)
  (cglue (b; pf)) 1 = 1
      transport_paths FFlr; apply equiv_p1_1q.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
ap
  (sig_rec
     (cdepdescent_rec
        {|
          cddcs_sect :=
            fun (a : A) (x : cd_fam Pe a) =>
            coeq (a; x);
          cddcs_e :=
            fun (b : B) (pf : cd_fam Pe (f b)) =>
            cglue (b; pf)
        |}))
  (ap
     (Coeq_rec {x : _ & fam_cdescent Pe x}
        (fun pat : {x : _ & cd_fam Pe x} =>
         (coeq pat.1; pat.2))
        (fun b0 : {H : B & cd_fam Pe (f H)} =>
         flatten_cd_glue b0.1 1)) (cglue (b; pf))) =
cglue (b; pf)
      rewrite Coeq_rec_beta_cglue.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
ap
  (sig_rec
     (cdepdescent_rec
        {|
          cddcs_sect :=
            fun (a : A) (x : cd_fam Pe a) =>
            coeq (a; x);
          cddcs_e :=
            fun (b : B) (pf : cd_fam Pe (f b)) =>
            cglue (b; pf)
        |})) (flatten_cd_glue b 1) = cglue (b; pf)
      lhs napply cdepdescent_rec_beta_cglue.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
cddcs_e
  {|
    cddcs_sect :=
      fun (a : A) (x : cd_fam Pe a) => coeq (a; x);
    cddcs_e :=
      fun (b : B) (pf : cd_fam Pe (f b)) =>
      cglue (b; pf)
  |} (b; pf).1 (b; pf).2 @
ap
  (cddcs_sect
     {|
       cddcs_sect :=
         fun (a : A) (x : cd_fam Pe a) => coeq (a; x);
       cddcs_e :=
         fun (b : B) (pf : cd_fam Pe (f b)) =>
         cglue (b; pf)
     |} (g (b; pf).1)) 1 = cglue (b; pf)
      napply concat_p1.
    -
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
Coeq_rec {x : _ & fam_cdescent Pe x}
  (fun pat : {x : _ & cd_fam Pe x} =>
   let x := pat in
   let a := x.1 in let x0 := x.2 in (coeq a; x0))
  (fun b0 : {H : B & cd_fam Pe (f H)} =>
   (fun (b : B) (pf : cd_fam Pe (f b)) =>
    flatten_cd_glue b 1
    :
    (let x :=
       functor_sigma f (fun a : B => idmap) (b; pf) in
     let a := x.1 in let x0 := x.2 in (coeq a; x0)) =
    (let x :=
       functor_sigma g (fun b1 : B => cd_e Pe b1)
         (b; pf) in
     let a := x.1 in let x0 := x.2 in (coeq a; x0)))
     b0.1 b0.2)
o sig_rec
    (cdepdescent_rec
       {|
         cddcs_sect :=
           fun (a : A) (x : cd_fam Pe a) =>
           coeq (a; x);
         cddcs_e :=
           fun (b : B) (pf : cd_fam Pe (f b)) =>
           cglue (b; pf)
           :
           (fun (a : A) (x : cd_fam Pe a) =>
            coeq (a; x)) (f b) pf =
           (fun (a : A) (x : cd_fam Pe a) =>
            coeq (a; x)) (g b) (cd_e Pe b pf)
       |}) == idmap intros [x px]; revert x px.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
forall (x : Coeq f g) (px : fam_cdescent Pe x),
Coeq_rec {x : _ & fam_cdescent Pe x}
  (fun pat : {x : _ & cd_fam Pe x} =>
   let x0 := pat in
   let a := x0.1 in let x1 := x0.2 in (coeq a; x1))
  (fun b0 : {H : B & cd_fam Pe (f H)} =>
   flatten_cd_glue b0.1 1)
  (sig_rec
     (cdepdescent_rec
        {|
          cddcs_sect :=
            fun (a : A) (x0 : cd_fam Pe a) =>
            coeq (a; x0);
          cddcs_e :=
            fun (b : B) (pf : cd_fam Pe (f b)) =>
            cglue (b; pf)
        |}) (x; px)) = (x; px)
      snapply cdepdescent_ind.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
cDepDescentSection
  (cdepdescent_fam
     (fun (x : Coeq f g) (px : fam_cdescent Pe x) =>
      Coeq_rec {x : _ & fam_cdescent Pe x}
        (fun pat : {x : _ & cd_fam Pe x} =>
         let x0 := pat in
         let a := x0.1 in
         let x1 := x0.2 in (coeq a; x1))
        (fun b0 : {H : B & cd_fam Pe (f H)} =>
         flatten_cd_glue b0.1 1)
        (sig_rec
           (cdepdescent_rec
              {|
                cddcs_sect :=
                  fun (a : A) (x0 : cd_fam Pe a) =>
                  coeq (a; x0);
                cddcs_e :=
                  fun (b : B) (pf : cd_fam Pe (f b))
                  => cglue (b; pf)
              |}) (x; px)) = (x; px)))
      snapply Build_cDepDescentSection.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
forall (a : A) (pa : cd_fam Pe a),
cdd_fam
  (cdepdescent_fam
     (fun (x : Coeq f g) (px : fam_cdescent Pe x) =>
      Coeq_rec {x : _ & fam_cdescent Pe x}
        (fun pat : {x : _ & cd_fam Pe x} =>
         let x0 := pat in
         let a0 := x0.1 in
         let x1 := x0.2 in (coeq a0; x1))
        (fun b0 : {H : B & cd_fam Pe (f H)} =>
         flatten_cd_glue b0.1 1)
        (sig_rec
           (cdepdescent_rec
              {|
                cddcs_sect :=
                  fun (a0 : A) (x0 : cd_fam Pe a0) =>
                  coeq (a0; x0);
                cddcs_e :=
                  fun (b : B) (pf : cd_fam Pe (f b))
                  => cglue (b; pf)
              |}) (x; px)) = (x; px))) a pa
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
forall (b : B) (pf : cd_fam Pe (f b)),
cdd_e
  (cdepdescent_fam
     (fun (x : Coeq f g) (px : fam_cdescent Pe x) =>
      Coeq_rec {x : _ & fam_cdescent Pe x}
        (fun pat : {x : _ & cd_fam Pe x} =>
         let x0 := pat in
         let a := x0.1 in
         let x1 := x0.2 in (coeq a; x1))
        (fun b0 : {H : B & cd_fam Pe (f H)} =>
         flatten_cd_glue b0.1 1)
        (sig_rec
           (cdepdescent_rec
              {|
                cddcs_sect :=
                  fun (a : A) (x0 : cd_fam Pe a) =>
                  coeq (a; x0);
                cddcs_e :=
                  fun (b0 : B)
                    (pf0 : cd_fam Pe (f b0)) =>
                  cglue (b0; pf0)
              |}) (x; px)) = (x; px))) b pf
  (?cdds_sect (f b) pf) =
?cdds_sect (g b) (cd_e Pe b pf)
      +
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
forall (a : A) (pa : cd_fam Pe a),
cdd_fam
  (cdepdescent_fam
     (fun (x : Coeq f g) (px : fam_cdescent Pe x) =>
      Coeq_rec {x : _ & fam_cdescent Pe x}
        (fun pat : {x : _ & cd_fam Pe x} =>
         let x0 := pat in
         let a0 := x0.1 in
         let x1 := x0.2 in (coeq a0; x1))
        (fun b0 : {H : B & cd_fam Pe (f H)} =>
         flatten_cd_glue b0.1 1)
        (sig_rec
           (cdepdescent_rec
              {|
                cddcs_sect :=
                  fun (a0 : A) (x0 : cd_fam Pe a0) =>
                  coeq (a0; x0);
                cddcs_e :=
                  fun (b : B) (pf : cd_fam Pe (f b))
                  => cglue (b; pf)
              |}) (x; px)) = (x; px))) a pa by intros a pa.
      +
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
forall (b : B) (pf : cd_fam Pe (f b)),
cdd_e
  (cdepdescent_fam
     (fun (x : Coeq f g) (px : fam_cdescent Pe x) =>
      Coeq_rec {x : _ & fam_cdescent Pe x}
        (fun pat : {x : _ & cd_fam Pe x} =>
         let x0 := pat in
         let a := x0.1 in
         let x1 := x0.2 in (coeq a; x1))
        (fun b0 : {H : B & cd_fam Pe (f H)} =>
         flatten_cd_glue b0.1 1)
        (sig_rec
           (cdepdescent_rec
              {|
                cddcs_sect :=
                  fun (a : A) (x0 : cd_fam Pe a) =>
                  coeq (a; x0);
                cddcs_e :=
                  fun (b0 : B)
                    (pf0 : cd_fam Pe (f b0)) =>
                  cglue (b0; pf0)
              |}) (x; px)) = (x; px))) b pf
  ((fun (a : A) (pa : cd_fam Pe a) => 1) (f b) pf) =
(fun (a : A) (pa : cd_fam Pe a) => 1) (g b)
  (cd_e Pe b pf) intros b pf; cbn.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
transportDD (fam_cdescent Pe)
  (fun (x : Coeq f g) (px : fam_cdescent Pe x) =>
   Coeq_rec {x : _ & fam_cdescent Pe x}
     (fun pat : {x : _ & cd_fam Pe x} =>
      (coeq pat.1; pat.2))
     (fun b0 : {H : B & cd_fam Pe (f H)} =>
      flatten_cd_glue b0.1 1)
     (sig_rec
        (cdepdescent_rec
           {|
             cddcs_sect :=
               fun (a : A) (x0 : cd_fam Pe a) =>
               coeq (a; x0);
             cddcs_e :=
               fun (b : B) (pf : cd_fam Pe (f b)) =>
               cglue (b; pf)
           |}) (x; px)) = (x; px)) (cglue b)
  (transport_fam_cdescent_cglue Pe b pf) 1 = 1
        lhs napply transportDD_is_transport.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
transport
  (fun ab : {x : _ & fam_cdescent Pe x} =>
   Coeq_rec {x : _ & fam_cdescent Pe x}
     (fun pat : {x : _ & cd_fam Pe x} =>
      (coeq pat.1; pat.2))
     (fun b0 : {H : B & cd_fam Pe (f H)} =>
      flatten_cd_glue b0.1 1)
     (sig_rec
        (cdepdescent_rec
           {|
             cddcs_sect :=
               fun (a : A) (x : cd_fam Pe a) =>
               coeq (a; x);
             cddcs_e :=
               fun (b : B) (pf : cd_fam Pe (f b)) =>
               cglue (b; pf)
           |}) (ab.1; ab.2)) = (ab.1; ab.2))
  (path_sigma' (fam_cdescent Pe) (cglue b)
     (transport_fam_cdescent_cglue Pe b pf)) 1 = 1
        transport_paths FFlr; apply equiv_p1_1q.
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
ap
  (Coeq_rec {x : _ & fam_cdescent Pe x}
     (fun pat : {x : _ & cd_fam Pe x} =>
      (coeq pat.1; pat.2))
     (fun b0 : {H : B & cd_fam Pe (f H)} =>
      flatten_cd_glue b0.1 1))
  (ap
     (sig_rec
        (cdepdescent_rec
           {|
             cddcs_sect :=
               fun (a : A) (x : cd_fam Pe a) =>
               coeq (a; x);
             cddcs_e :=
               fun (b : B) (pf : cd_fam Pe (f b)) =>
               cglue (b; pf)
           |}))
     (path_sigma' (fam_cdescent Pe) (cglue b)
        (transport_fam_cdescent_cglue Pe b pf))) =
path_sigma' (fam_cdescent Pe) (cglue b)
  (transport_fam_cdescent_cglue Pe b pf)
        rewrite <- (concat_p1 (transport_fam_cdescent_cglue _ _ _)).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
ap
  (Coeq_rec {x : _ & fam_cdescent Pe x}
     (fun pat : {x : _ & cd_fam Pe x} =>
      (coeq pat.1; pat.2))
     (fun b0 : {H : B & cd_fam Pe (f H)} =>
      flatten_cd_glue b0.1 1))
  (ap
     (sig_rec
        (cdepdescent_rec
           {|
             cddcs_sect :=
               fun (a : A) (x : cd_fam Pe a) =>
               coeq (a; x);
             cddcs_e :=
               fun (b : B) (pf : cd_fam Pe (f b)) =>
               cglue (b; pf)
           |}))
     (path_sigma' (fam_cdescent Pe) (cglue b)
        (transport_fam_cdescent_cglue Pe b pf @ 1))) =
path_sigma' (fam_cdescent Pe) (cglue b)
  (transport_fam_cdescent_cglue Pe b pf @ 1)
        rewrite cdepdescent_rec_beta_cglue. (* This needs to be in the form [transport_fam_cdescent_cglue Pe r pa @ p] to work, and the other [@ 1] introduced comes in handy as well. *)
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
ap
  (Coeq_rec {x : _ & fam_cdescent Pe x}
     (fun pat : {x : _ & cd_fam Pe x} =>
      (coeq pat.1; pat.2))
     (fun b0 : {H : B & cd_fam Pe (f H)} =>
      flatten_cd_glue b0.1 1))
  (cddcs_e
     {|
       cddcs_sect :=
         fun (a : A) (x : cd_fam Pe a) => coeq (a; x);
       cddcs_e :=
         fun (b : B) (pf : cd_fam Pe (f b)) =>
         cglue (b; pf)
     |} b pf @
   ap
     (cddcs_sect
        {|
          cddcs_sect :=
            fun (a : A) (x : cd_fam Pe a) =>
            coeq (a; x);
          cddcs_e :=
            fun (b : B) (pf : cd_fam Pe (f b)) =>
            cglue (b; pf)
        |} (g b)) 1) =
path_sigma' (fam_cdescent Pe) (cglue b)
  (transport_fam_cdescent_cglue Pe b pf @ 1)
        lhs napply (ap _ (concat_p1 _)).
H: Univalence
A, B: Type
f, g: B -> A
Pe: cDescent f g
b: B
pf: cd_fam Pe (f b)
ap
  (Coeq_rec {x : _ & fam_cdescent Pe x}
     (fun pat : {x : _ & cd_fam Pe x} =>
      (coeq pat.1; pat.2))
     (fun b0 : {H : B & cd_fam Pe (f H)} =>
      flatten_cd_glue b0.1 1))
  (cddcs_e
     {|
       cddcs_sect :=
         fun (a : A) (x : cd_fam Pe a) => coeq (a; x);
       cddcs_e :=
         fun (b : B) (pf : cd_fam Pe (f b)) =>
         cglue (b; pf)
     |} b pf) =
path_sigma' (fam_cdescent Pe) (cglue b)
  (transport_fam_cdescent_cglue Pe b pf @ 1)
        exact (Coeq_rec_beta_cglue _ _ _ (b; pf)).
  Defined.

End Flattening.

(** ** Characterization of path spaces *)

(** A pointed type family over a coequalizer has an identity system structure precisely when its associated descent data satisfies Kraus and von Raumer's induction principle, https://arxiv.org/pdf/1901.06022. *)

Section Paths.

  (** Let [f g : B -> A] be a parallel pair, with a distinguished point [a0 : A].  Let [Pe : cDescent f g] be descent data over [f g] with a distinguished point [p0 : cd_fam Pe a0].  Assume that any dependent descent data [Qe : cDepDescent Pe] with a distinguished point [q0 : cdd_fam Qe a0 p0] has a section that respects the distinguished points.  This is the induction principle provided by Kraus and von Raumer. *)
  Context `{Univalence} {A B: Type} {f g : B -> A} (a0 : A)
    (Pe : cDescent f g) (p0 : cd_fam Pe a0)
    (based_cdepdescent_ind : forall (Qe : cDepDescent Pe) (q0 : cdd_fam Qe a0 p0),
      cDepDescentSection Qe)
    (based_cdepdescent_ind_beta : forall (Qe : cDepDescent Pe) (q0 : cdd_fam Qe a0 p0),
      cdds_sect (based_cdepdescent_ind Qe q0) a0 p0 = q0).

  (** Under these hypotheses, we get an identity system structure on [fam_cdescent Pe]. *)
  Local Instance idsys_flatten_cdescent
    : @IsIdentitySystem _ (coeq a0) (fam_cdescent Pe) p0.
H: Univalence
A, B: Type
f, g: B -> A
a0: A
Pe: cDescent f g
p0: cd_fam Pe a0
based_cdepdescent_ind: forall Qe : cDepDescent Pe,
cdd_fam Qe a0 p0 ->
cDepDescentSection Qe
based_cdepdescent_ind_beta: forall
(Qe : cDepDescent Pe)
(q0 : cdd_fam Qe a0 p0),
cdds_sect
  (based_cdepdescent_ind
     Qe q0) a0 p0 = q0
IsIdentitySystem (fam_cdescent Pe) p0
  Proof.
H: Univalence
A, B: Type
f, g: B -> A
a0: A
Pe: cDescent f g
p0: cd_fam Pe a0
based_cdepdescent_ind: forall Qe : cDepDescent Pe,
cdd_fam Qe a0 p0 ->
cDepDescentSection Qe
based_cdepdescent_ind_beta: forall
(Qe : cDepDescent Pe)
(q0 : cdd_fam Qe a0 p0),
cdds_sect
  (based_cdepdescent_ind
     Qe q0) a0 p0 = q0
IsIdentitySystem (fam_cdescent Pe) p0
    snapply Build_IsIdentitySystem.
H: Univalence
A, B: Type
f, g: B -> A
a0: A
Pe: cDescent f g
p0: cd_fam Pe a0
based_cdepdescent_ind: forall Qe : cDepDescent Pe,
cdd_fam Qe a0 p0 ->
cDepDescentSection Qe
based_cdepdescent_ind_beta: forall
(Qe : cDepDescent Pe)
(q0 : cdd_fam Qe a0 p0),
cdds_sect
  (based_cdepdescent_ind
     Qe q0) a0 p0 = q0
forall
D : forall a : Coeq f g, fam_cdescent Pe a -> Type,
D (coeq a0) p0 ->
forall (a : Coeq f g) (r : fam_cdescent Pe a), D a r
H: Univalence
A, B: Type
f, g: B -> A
a0: A
Pe: cDescent f g
p0: cd_fam Pe a0
based_cdepdescent_ind: forall Qe : cDepDescent Pe,
cdd_fam Qe a0 p0 ->
cDepDescentSection Qe
based_cdepdescent_ind_beta: forall
(Qe : cDepDescent Pe)
(q0 : cdd_fam Qe a0 p0),
cdds_sect
  (based_cdepdescent_ind
     Qe q0) a0 p0 = q0
forall
(D : forall a : Coeq f g, fam_cdescent Pe a -> Type)
(d : D (coeq a0) p0), 
?idsys_ind D d (coeq a0) p0 = d
    -
H: Univalence
A, B: Type
f, g: B -> A
a0: A
Pe: cDescent f g
p0: cd_fam Pe a0
based_cdepdescent_ind: forall Qe : cDepDescent Pe,
cdd_fam Qe a0 p0 ->
cDepDescentSection Qe
based_cdepdescent_ind_beta: forall
(Qe : cDepDescent Pe)
(q0 : cdd_fam Qe a0 p0),
cdds_sect
  (based_cdepdescent_ind
     Qe q0) a0 p0 = q0
forall
D : forall a : Coeq f g, fam_cdescent Pe a -> Type,
D (coeq a0) p0 ->
forall (a : Coeq f g) (r : fam_cdescent Pe a), D a r intros Q q0 x p.
H: Univalence
A, B: Type
f, g: B -> A
a0: A
Pe: cDescent f g
p0: cd_fam Pe a0
based_cdepdescent_ind: forall Qe : cDepDescent Pe,
cdd_fam Qe a0 p0 ->
cDepDescentSection Qe
based_cdepdescent_ind_beta: forall
(Qe : cDepDescent Pe)
(q0 : cdd_fam Qe a0 p0),
cdds_sect
  (based_cdepdescent_ind
     Qe q0) a0 p0 = q0
Q: forall a : Coeq f g, fam_cdescent Pe a -> Type
q0: Q (coeq a0) p0
x: Coeq f g
p: fam_cdescent Pe x
Q x p
      snapply cdepdescent_ind.
H: Univalence
A, B: Type
f, g: B -> A
a0: A
Pe: cDescent f g
p0: cd_fam Pe a0
based_cdepdescent_ind: forall Qe : cDepDescent Pe,
cdd_fam Qe a0 p0 ->
cDepDescentSection Qe
based_cdepdescent_ind_beta: forall
(Qe : cDepDescent Pe)
(q0 : cdd_fam Qe a0 p0),
cdds_sect
  (based_cdepdescent_ind
     Qe q0) a0 p0 = q0
Q: forall a : Coeq f g, fam_cdescent Pe a -> Type
q0: Q (coeq a0) p0
x: Coeq f g
p: fam_cdescent Pe x
cDepDescentSection (cdepdescent_fam Q)
      by apply based_cdepdescent_ind.
    -
H: Univalence
A, B: Type
f, g: B -> A
a0: A
Pe: cDescent f g
p0: cd_fam Pe a0
based_cdepdescent_ind: forall Qe : cDepDescent Pe,
cdd_fam Qe a0 p0 ->
cDepDescentSection Qe
based_cdepdescent_ind_beta: forall
(Qe : cDepDescent Pe)
(q0 : cdd_fam Qe a0 p0),
cdds_sect
  (based_cdepdescent_ind
     Qe q0) a0 p0 = q0
forall
(D : forall a : Coeq f g, fam_cdescent Pe a -> Type)
(d : D (coeq a0) p0),
(fun
   (Q : forall a : Coeq f g, fam_cdescent Pe a -> Type)
   (q0 : Q (coeq a0) p0) (x : Coeq f g)
   (p : fam_cdescent Pe x) =>
 cdepdescent_ind
   (based_cdepdescent_ind (cdepdescent_fam Q) q0) x p)
  D d (coeq a0) p0 = d intros Q q0; cbn.
H: Univalence
A, B: Type
f, g: B -> A
a0: A
Pe: cDescent f g
p0: cd_fam Pe a0
based_cdepdescent_ind: forall Qe : cDepDescent Pe,
cdd_fam Qe a0 p0 ->
cDepDescentSection Qe
based_cdepdescent_ind_beta: forall
(Qe : cDepDescent Pe)
(q0 : cdd_fam Qe a0 p0),
cdds_sect
  (based_cdepdescent_ind
     Qe q0) a0 p0 = q0
Q: forall a : Coeq f g, fam_cdescent Pe a -> Type
q0: Q (coeq a0) p0
cdepdescent_ind
  (based_cdepdescent_ind (cdepdescent_fam Q) q0)
  (coeq a0) p0 = q0
      napply (based_cdepdescent_ind_beta (cdepdescent_fam Q)).
  Defined.

  (** It follows that the fibers [fam_cdescent Pe x] are equivalent to path spaces [(coeq a0) = x]. *)
  Definition induced_fam_cd_equiv_path (x : Coeq f g)
    : (coeq a0) = x <~> fam_cdescent Pe x
    := @equiv_transport_identitysystem _ (coeq a0) (fam_cdescent Pe) p0 _ x.

End Paths.