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.

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.

(** ** 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
    nrapply 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)
    nrapply 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_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
  nrapply 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))
  refine (transport_paths_FlFr (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 == 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 (f b))) @
ap (functor_coeq h' k' p' q') (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 == 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 (s (f b)) @
ap (functor_coeq h' k' p' q') (cglue b) =
ap (functor_coeq h k p q) (cglue 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 == 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 (s (f b)) @
((ap coeq (p' b) @ cglue (h' b)) @ ap coeq (q' b)^) =
((ap coeq (p b) @ cglue (h b)) @ ap coeq (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 == 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 (s (f b))
@' (ap coeq (p' b)
    @' cglue (h' b)
    @' ap coeq (q' b)^) =
ap coeq (p b)
@' cglue (h b)
@' ap coeq (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 == 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 (s (f b))
@' ap coeq (p' b)
@' cglue (h' b)
@' ap coeq (q' b)^ =
ap coeq (p b)
@' cglue (h b)
@' ap coeq (q b)^
@' ap coeq (s (g 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 (s (f b)
         @' p' b)
@' cglue (h' b)
@' ap coeq (q' b)^ =
ap coeq (p b)
@' cglue (h b)
@' ap coeq (q b)^
@' ap coeq (s (g b))
  rewrite u, ap_pp, !concat_pp_p; apply whiskerL; 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 (ap f' (r b))
@' cglue (h' b)
@' ap coeq (q' b)^ =
cglue (h b)
@' ap coeq (q b)^
@' ap coeq (s (g b))
  rewrite ap_V; apply moveR_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 (ap f' (r b))
@' cglue (h' b) =
cglue (h b)
@' ap coeq (q b)^
@' ap coeq (s (g b))
@' ap coeq (q' b)
  rewrite !concat_pp_p, <- (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
ap coeq (ap f' (r b))
@' cglue (h' b) =
cglue (h b)
@' (ap coeq (q b)^
    @' ap coeq (s (g b)
                @' q' b))
  rewrite v, ap_pp, ap_V, 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
ap coeq (ap f' (r b))
@' cglue (h' b) = cglue (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 == 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 (fun x : B' => coeq (f' x)) (r b)
@' cglue (h' b) =
cglue (h b)
@' ap (fun x : B' => coeq (g' x)) (r 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.

  Global 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
    snrapply 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
      snrapply 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)
      snrapply 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')
        nrapply (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 nrapply (_ @@ 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 nrapply (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'
    nrapply 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'
    nrapply 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.

(** ** Flattening *)

(** The flattening lemma for coequalizers follows from the flattening lemma for graph quotients. *)

Section Flattening.

  Context `{Univalence} {B A : Type} {f g : B -> A}
    (F : A -> Type) (e : forall b, F (f b) <~> F (g b)).

  Definition coeq_flatten_fam : Coeq f g -> Type
    := Coeq_rec Type F (fun x => path_universe (e x)).

  Local Definition R (a b : A) := {x : B & (f x = a) * (g x = b)}.

  Local Definition e' (a b : A) : R a b -> (F a <~> F b).
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
a, b: A
R a b -> F a <~> F b
  Proof.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
a, b: A
R a b -> F a <~> F b
    intros [x [[] []]]; exact (e x).
  Defined.

  Definition equiv_coeq_flatten
    : sig coeq_flatten_fam
    <~> Coeq (functor_sigma f (fun _ => idmap)) (functor_sigma g e).
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
{x : _ & coeq_flatten_fam x} <~>
Coeq (functor_sigma f (fun a : B => idmap))
  (functor_sigma g (fun b : B => e b))
  Proof.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
{x : _ & coeq_flatten_fam x} <~>
Coeq (functor_sigma f (fun a : B => idmap))
  (functor_sigma g (fun b : B => e b))
    snrefine (_ oE equiv_gq_flatten F e' oE _).
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
GraphQuotient
  (fun a b : {x : _ & F x} =>
   {r : R a.1 b.1 & e' a.1 b.1 r a.2 = b.2}) <~>
Coeq (functor_sigma f (fun a : B => idmap))
  (functor_sigma g (fun b : B => e b))
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
{x : _ & coeq_flatten_fam x} <~>
{x : _ & DGraphQuotient F e' x}
    -
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
GraphQuotient
  (fun a b : {x : _ & F x} =>
   {r : R a.1 b.1 & e' a.1 b.1 r a.2 = b.2}) <~>
Coeq (functor_sigma f (fun a : B => idmap))
  (functor_sigma g (fun b : B => e b)) snrapply equiv_functor_gq.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
{x : _ & F x} <~> {x : _ & F x}
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
forall a b : {x : _ & F x},
(fun a0 b0 : {x : _ & F x} =>
 {r : R a0.1 b0.1 & e' a0.1 b0.1 r a0.2 = b0.2}) a b <~>
(fun a0 b0 : {x : _ & F x} =>
 {x : {H : B & F (f H)} &
 (functor_sigma f (fun a1 : B => idmap) x = a0) *
 (functor_sigma g (fun b1 : B => e b1) x = b0)})
  (?f0 a) (?f0 b)
      1: reflexivity.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
forall a b : {x : _ & F x},
(fun a0 b0 : {x : _ & F x} =>
 {r : R a0.1 b0.1 & e' a0.1 b0.1 r a0.2 = b0.2}) a b <~>
(fun a0 b0 : {x : _ & F x} =>
 {x : {H : B & F (f H)} &
 (functor_sigma f (fun a1 : B => idmap) x = a0) *
 (functor_sigma g (fun b1 : B => e b1) x = b0)})
  (1%equiv a) (1%equiv b)
      intros [a x] [b y]; simpl.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
a: A
x: F a
b: A
y: F b
{r : R a b & e' a b r x = y} <~>
{x0 : {H : B & F (f H)} &
(functor_sigma f (fun a : B => idmap) x0 = (a; x)) *
(functor_sigma g (fun b : B => e b) x0 = (b; y))}
      unfold functor_sigma.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
a: A
x: F a
b: A
y: F b
{r : R a b & e' a b r x = y} <~>
{x0 : {H : B & F (f H)} &
((f x0.1; x0.2) = (a; x)) *
((g x0.1; e x0.1 x0.2) = (b; y))}
      (* We use [equiv_path_sigma] twice on the RHS: *)
      equiv_via {x0 : {H0 : B & F (f H0)} &
                      {p : f x0.1 = a & p # x0.2 = x} * {q : g x0.1 = b & q # e x0.1 x0.2 = y}}.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
a: A
x: F a
b: A
y: F b
{r : R a b & e' a b r x = y} <~>
{x0 : {H0 : B & F (f H0)} &
{p : f x0.1 = a & transport F p x0.2 = x} *
{q : g x0.1 = b & transport F q (e x0.1 x0.2) = y}}
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
a: A
x: F a
b: A
y: F b
{x0 : {H0 : B & F (f H0)} &
{p : f x0.1 = a & transport F p x0.2 = x} *
{q : g x0.1 = b & transport F q (e x0.1 x0.2) = y}} <~>
{x0 : {H : B & F (f H)} &
((f x0.1; x0.2) = (a; x)) *
((g x0.1; e x0.1 x0.2) = (b; y))}
      2: {
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
a: A
x: F a
b: A
y: F b
{x0 : {H0 : B & F (f H0)} &
{p : f x0.1 = a & transport F p x0.2 = x} *
{q : g x0.1 = b & transport F q (e x0.1 x0.2) = y}} <~>
{x0 : {H : B & F (f H)} &
((f x0.1; x0.2) = (a; x)) *
((g x0.1; e x0.1 x0.2) = (b; y))} nrapply equiv_functor_sigma_id; intros [c z]; cbn.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
a: A
x: F a
b: A
y: F b
c: B
z: F (f c)
{p : f c = a & transport F p z = x} *
{q : g c = b & transport F q (e c z) = y} <~>
((f c; z) = (a; x)) * ((g c; e c z) = (b; y))
           nrapply equiv_functor_prod'.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
a: A
x: F a
b: A
y: F b
c: B
z: F (f c)
{p : f c = a & transport F p z = x} <~>
(f c; z) = (a; x)
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
a: A
x: F a
b: A
y: F b
c: B
z: F (f c)
{q : g c = b & transport F q (e c z) = y} <~>
(g c; e c z) = (b; y)
           all: apply (equiv_path_sigma _ (_; _) (_; _)). }
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
a: A
x: F a
b: A
y: F b
{r : R a b & e' a b r x = y} <~>
{x0 : {H0 : B & F (f H0)} &
{p : f x0.1 = a & transport F p x0.2 = x} *
{q : g x0.1 = b & transport F q (e x0.1 x0.2) = y}}
      (* [make_equiv_contr_basedpaths.] handles the rest, but is slow, so we do some steps manually. *)
      (* The RHS can be shuffled to this form: *)
      equiv_via {r : R a b & { x02 : F (f r.1) & (transport F (fst r.2) x02 = x) *
                                                 (transport F (snd r.2) (e r.1 x02) = y)}}.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
a: A
x: F a
b: A
y: F b
{r : R a b & e' a b r x = y} <~>
{r : R a b &
{x02 : F (f r.1) &
(transport F (fst r.2) x02 = x) *
(transport F (snd r.2) (e r.1 x02) = y)}}
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
a: A
x: F a
b: A
y: F b
{r : R a b &
{x02 : F (f r.1) &
(transport F (fst r.2) x02 = x) *
(transport F (snd r.2) (e r.1 x02) = y)}} <~>
{x0 : {H0 : B & F (f H0)} &
{p : f x0.1 = a & transport F p x0.2 = x} *
{q : g x0.1 = b & transport F q (e x0.1 x0.2) = y}}
      2: make_equiv.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
a: A
x: F a
b: A
y: F b
{r : R a b & e' a b r x = y} <~>
{r : R a b &
{x02 : F (f r.1) &
(transport F (fst r.2) x02 = x) *
(transport F (snd r.2) (e r.1 x02) = y)}}
      (* Three path contractions handle the rest. *)
      nrapply equiv_functor_sigma_id; intros [c [p q]].
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
a: A
x: F a
b: A
y: F b
c: B
p: f c = a
q: g c = b
e' a b (c; (p, q)) x = y <~>
{x02 : F (f (c; (p, q)).1) &
(transport F (fst (c; (p, q)).2) x02 = x) *
(transport F (snd (c; (p, q)).2) (e (c; (p, q)).1 x02) =
 y)}
      destruct p, q; unfold e'; simpl.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
c: B
x: F (f c)
y: F (g c)
e c x = y <~>
{x02 : F (f c) & (x02 = x) * (e c x02 = y)}
      make_equiv_contr_basedpaths.
    -
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
{x : _ & coeq_flatten_fam x} <~>
{x : _ & DGraphQuotient F e' x} apply equiv_functor_sigma_id; intros x.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
x: Coeq f g
coeq_flatten_fam x <~> DGraphQuotient F e' x
      apply equiv_path.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
x: Coeq f g
coeq_flatten_fam x = DGraphQuotient F e' x
      revert x; snrapply Coeq_ind.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
forall a : A,
(fun w : Coeq f g =>
 coeq_flatten_fam w = DGraphQuotient F e' w) (coeq a)
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
forall b : B,
transport
  (fun w : Coeq f g =>
   coeq_flatten_fam w = DGraphQuotient F e' w)
  (cglue b) (?coeq' (f b)) = ?coeq' (g b)
      1: reflexivity.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
forall b : B,
transport
  (fun w : Coeq f g =>
   coeq_flatten_fam w = DGraphQuotient F e' w)
  (cglue b) ((fun a : A => 1) (f b)) =
(fun a : A => 1) (g b)
      simpl.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
forall b : B,
transport
  (fun w : Coeq f g =>
   coeq_flatten_fam w = DGraphQuotient F e' w)
  (cglue b) 1 = 1
      intros b.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
b: B
transport
  (fun w : Coeq f g =>
   coeq_flatten_fam w = DGraphQuotient F e' w)
  (cglue b) 1 = 1
      snrapply (dpath_path_FlFr (cglue b)).
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
b: B
1 @ ap (DGraphQuotient F e') (cglue b) =
ap coeq_flatten_fam (cglue b) @ 1
      apply equiv_1p_q1.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
b: B
ap (DGraphQuotient F e') (cglue b) =
ap coeq_flatten_fam (cglue b)
      rhs nrapply Coeq_rec_beta_cglue.
H: Univalence
B, A: Type
f, g: B -> A
F: A -> Type
e: forall b : B, F (f b) <~> F (g b)
b: B
ap (DGraphQuotient F e') (cglue b) =
path_universe (e b)
      exact (GraphQuotient_rec_beta_gqglue _
               (fun a b s => path_universe (e' a b s)) _ _ _).
  Defined.

End Flattening.