CoeqUnivProp.v

Require Import Basics.Overture.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Basics.Tactics.
Require Import Basics.PathGroupoids.
Require Import Types.Paths.
Require Import Colimits.Coeq.
Require Import Cubical.DPath.
Require Import Cubical.DPathSquare.
Require Import WildCat.Core.
Require Import WildCat.Displayed.
Require Import WildCat.Equiv.
Require Import WildCat.EquivGpd.
Require Import WildCat.Forall.
Require Import WildCat.NatTrans.
Require Import WildCat.Paths.
Require Import WildCat.FunctorCat.
Require Import WildCat.ZeroGroupoid.

(* Successful typeclass inference in this file is sensitive to the order of imports; in particular FunctorCat should not be the last import. *)

(** Using wild 0-groupoids, the universal property can be proven without funext. A simple equivalence of 0-groupoids between [Coeq f g -> P] and [{ h : A -> P & h o f == h o g }] would not carry all the higher-dimensional information, but if we generalize it to dependent functions, then it does suffice. *)
Section UnivProp.
  Context {B A : Type} (f g : B -> A) (P : Coeq f g -> Type).

  (** This allows Coq to infer 0-groupoid structures of the form [@isgraph_forall C P (fun c => isgraph_paths (P c))] on any type of the form [forall c, P c].  [isgraph_paths] is not a global instance.  [isgraph_total] is, but we need to adjust the priority.  The other needed ingredients are all global instances. *)
  Local Existing Instances isgraph_total | 1.
  Local Existing Instances isgraph_paths | 2.

  (** The domain of the equivalence: sections of [P] over [Coeq f g]. Coq correctly infers the 0-groupoid structure [@isgraph_forall (Coeq f g) P (fun z : Coeq f g => isgraph_paths (P z))]. *)
  Definition Coeq_ind_type := forall z : Coeq f g, P z.

  (** The codomain of the equivalence is a sigma-groupoid of this family: *)
  Definition Coeq_ind_data (h : forall a : A, P (coeq a))
    := forall b : B, DPath P (cglue b) (h (f b)) (h (g b)).

  (** We consider [Coeq_ind_data] to be a displayed 0-groupoid, where objects over [h : forall a : A, P (coeq a)] are dependent paths as defined above and morphisms over [p : h == k] are witnesses that [p] commutes with the homotopies over [h] and [k]. *)
  Local Instance isdgraph_Coeq_ind_data : IsDGraph Coeq_ind_data.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
IsDGraph Coeq_ind_data
  Proof.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
IsDGraph Coeq_ind_data
    intros h k p r s.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall a : A, P (coeq a)
p: h $-> k
r: Coeq_ind_data h
s: Coeq_ind_data k
Type
    exact (forall b, ap (transport P (cglue b)) (p (f b)) @ s b = r b @ p (g b)).
  Defined.

  Local Instance isd01cat_Coeq_ind_data : IsD01Cat Coeq_ind_data.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
IsD01Cat Coeq_ind_data
  Proof.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
IsD01Cat Coeq_ind_data
    napply Build_IsD01Cat.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
forall (a : forall a : A, P (coeq a))
(a' : Coeq_ind_data a), DHom (Id a) a' a'
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
forall (a : forall a : A, P (coeq a))
(b c : forall a0 : A, P (coeq a0)) (g0 : b $-> c)
(f0 : a $-> b) (a' : Coeq_ind_data a)
(b' : Coeq_ind_data b) (c' : Coeq_ind_data c),
DHom g0 b' c' ->
DHom f0 a' b' -> DHom (g0 $o f0) a' c'
    -B, A: Type
f, g: B -> A
P: Coeq f g -> Type
forall (a : forall a : A, P (coeq a))
(a' : Coeq_ind_data a), DHom (Id a) a' a' intros h h' b; exact (concat_1p_p1 _).
    -B, A: Type
f, g: B -> A
P: Coeq f g -> Type
forall (a : forall a : A, P (coeq a))
(b c : forall a0 : A, P (coeq a0)) (g0 : b $-> c)
(f0 : a $-> b) (a' : Coeq_ind_data a)
(b' : Coeq_ind_data b) (c' : Coeq_ind_data c),
DHom g0 b' c' ->
DHom f0 a' b' -> DHom (g0 $o f0) a' c' intros h k j p q h' k' j' p' q' b.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k, j: forall a : A, P (coeq a)
p: k $-> j
q: h $-> k
h': Coeq_ind_data h
k': Coeq_ind_data k
j': Coeq_ind_data j
p': DHom p k' j'
q': DHom q h' k'
b: B
ap (transport P (cglue b)) ((p $o q) (f b)) @ j' b =
h' b @ (p $o q) (g b)
      lhs napply ap_pp_p.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k, j: forall a : A, P (coeq a)
p: k $-> j
q: h $-> k
h': Coeq_ind_data h
k': Coeq_ind_data k
j': Coeq_ind_data j
p': DHom p k' j'
q': DHom q h' k'
b: B
ap (transport P (cglue b)) (q (f b)) @
(ap (transport P (cglue b)) (p (f b)) @ j' b) =
h' b @ (p $o q) (g b)
      lhs napply (whiskerL _ (p' b)).B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k, j: forall a : A, P (coeq a)
p: k $-> j
q: h $-> k
h': Coeq_ind_data h
k': Coeq_ind_data k
j': Coeq_ind_data j
p': DHom p k' j'
q': DHom q h' k'
b: B
ap (transport P (cglue b)) (q (f b)) @
(k' b @ p (g b)) = h' b @ (p $o q) (g b)
      lhs napply concat_p_pp.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k, j: forall a : A, P (coeq a)
p: k $-> j
q: h $-> k
h': Coeq_ind_data h
k': Coeq_ind_data k
j': Coeq_ind_data j
p': DHom p k' j'
q': DHom q h' k'
b: B
(ap (transport P (cglue b)) (q (f b)) @ k' b) @
p (g b) = h' b @ (p $o q) (g b)
      lhs napply (whiskerR (q' b)).B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k, j: forall a : A, P (coeq a)
p: k $-> j
q: h $-> k
h': Coeq_ind_data h
k': Coeq_ind_data k
j': Coeq_ind_data j
p': DHom p k' j'
q': DHom q h' k'
b: B
(h' b @ q (g b)) @ p (g b) = h' b @ (p $o q) (g b)
      napply concat_pp_p.
  Defined.

  Local Instance isd0gpd_Coeq_ind_data : IsD0Gpd Coeq_ind_data.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
IsD0Gpd Coeq_ind_data
  Proof.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
IsD0Gpd Coeq_ind_data
    intros h k p r s p' b.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall a : A, P (coeq a)
p: h $== k
r: Coeq_ind_data h
s: Coeq_ind_data k
p': DHom p r s
b: B
ap (transport P (cglue b)) (p^$ (f b)) @ r b =
s b @ p^$ (g b)
    lhs napply (whiskerR (ap_V _ _)).B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall a : A, P (coeq a)
p: h $== k
r: Coeq_ind_data h
s: Coeq_ind_data k
p': DHom p r s
b: B
(ap (transport P (cglue b)) (p (f b)))^ @ r b =
s b @ p^$ (g b)
    napply moveL_pV.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall a : A, P (coeq a)
p: h $== k
r: Coeq_ind_data h
s: Coeq_ind_data k
p': DHom p r s
b: B
((ap (transport P (cglue b)) (p (f b)))^ @ r b) @
p (g b) = s b
    lhs napply concat_pp_p.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall a : A, P (coeq a)
p: h $== k
r: Coeq_ind_data h
s: Coeq_ind_data k
p': DHom p r s
b: B
(ap (transport P (cglue b)) (p (f b)))^ @
(r b @ p (g b)) = s b
    lhs napply (whiskerL _ (p' b)^).B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall a : A, P (coeq a)
p: h $== k
r: Coeq_ind_data h
s: Coeq_ind_data k
p': DHom p r s
b: B
(ap (transport P (cglue b)) (p (f b)))^ @
(ap (transport P (cglue b)) (p (f b)) @ s b) = s b
    lhs napply concat_p_pp.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall a : A, P (coeq a)
p: h $== k
r: Coeq_ind_data h
s: Coeq_ind_data k
p': DHom p r s
b: B
((ap (transport P (cglue b)) (p (f b)))^ @
 ap (transport P (cglue b)) (p (f b))) @ s b = s b
    lhs napply (whiskerR (concat_Vp _)).B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall a : A, P (coeq a)
p: h $== k
r: Coeq_ind_data h
s: Coeq_ind_data k
p': DHom p r s
b: B
1 @ s b = s b
    napply concat_1p.
  Defined.

  (** Here is the functor. The domain is the fully-applied type of [Coeq_ind]: sections of [P] over [Coeq f g]. The codomain consists of input data for [Coeq_ind] given a 0-groupoid structure via [is0gpd_total]. *)
  Definition Coeq_ind_inv : Coeq_ind_type -> sig Coeq_ind_data.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
Coeq_ind_type -> {x : _ & Coeq_ind_data x}
  Proof.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
Coeq_ind_type -> {x : _ & Coeq_ind_data x}
    intros h.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: Coeq_ind_type
{x : _ & Coeq_ind_data x}
    exists (h o coeq).B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: Coeq_ind_type
Coeq_ind_data (fun x : A => h (coeq x))
    intros b.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: Coeq_ind_type
b: B
DPath P (cglue b) (h (coeq (f b))) (h (coeq (g b)))
    exact (apD h (cglue b)).
  Defined.

  (** Use [Set Printing Implicit] to see the 0-groupoid structures described above. *)
  Local Instance is0functor_Coeq_ind_inv : Is0Functor Coeq_ind_inv.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
Is0Functor Coeq_ind_inv
  Proof.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
Is0Functor Coeq_ind_inv
    napply Build_Is0Functor.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
forall a b : Coeq_ind_type,
(a $-> b) -> Coeq_ind_inv a $-> Coeq_ind_inv b
    intros h k p.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: Coeq_ind_type
p: h $-> k
Coeq_ind_inv h $-> Coeq_ind_inv k
    exists (p o coeq).B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: Coeq_ind_type
p: h $-> k
DHom (fun x : A => p (coeq x)) (Coeq_ind_inv h).2
  (Coeq_ind_inv k).2
    intros b.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: Coeq_ind_type
p: h $-> k
b: B
ap (transport P (cglue b)) (p (coeq (f b))) @
(Coeq_ind_inv k).2 b =
(Coeq_ind_inv h).2 b @ p (coeq (g b))
    napply moveL_pM.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: Coeq_ind_type
p: h $-> k
b: B
(ap (transport P (cglue b)) (p (coeq (f b))) @
 (Coeq_ind_inv k).2 b) @ (p (coeq (g b)))^ =
apD h (cglue b)
    exact ((apD_homotopic p (cglue b))^).
  Defined.

  Local Instance issurjinj_Coeq_ind_inv : IsSurjInj Coeq_ind_inv.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
IsSurjInj Coeq_ind_inv
  Proof.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
IsSurjInj Coeq_ind_inv
    napply Build_IsSurjInj.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
SplEssSurj Coeq_ind_inv
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
forall x y : Coeq_ind_type,
Coeq_ind_inv x $== Coeq_ind_inv y -> x $== y
    -B, A: Type
f, g: B -> A
P: Coeq f g -> Type
SplEssSurj Coeq_ind_inv intros [h r].B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall a : A, P (coeq a)
r: Coeq_ind_data h
{a : Coeq_ind_type & Coeq_ind_inv a $== (h; r)}
      exists (Coeq_ind P h r).B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall a : A, P (coeq a)
r: Coeq_ind_data h
Coeq_ind_inv (Coeq_ind P h r) $== (h; r)
      exists (fun a => idpath).B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall a : A, P (coeq a)
r: Coeq_ind_data h
DHom (fun a : A => 1)
  (Coeq_ind_inv (Coeq_ind P h r)).2 r
      intros b.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall a : A, P (coeq a)
r: Coeq_ind_data h
b: B
ap (transport P (cglue b)) 1 @ r b =
(Coeq_ind_inv (Coeq_ind P h r)).2 b @ 1
      apply equiv_1p_q1.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall a : A, P (coeq a)
r: Coeq_ind_data h
b: B
r b = (Coeq_ind_inv (Coeq_ind P h r)).2 b
      symmetry.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall a : A, P (coeq a)
r: Coeq_ind_data h
b: B
(Coeq_ind_inv (Coeq_ind P h r)).2 b = r b
      napply Coeq_ind_beta_cglue.
    -B, A: Type
f, g: B -> A
P: Coeq f g -> Type
forall x y : Coeq_ind_type,
Coeq_ind_inv x $== Coeq_ind_inv y -> x $== y intros h k [p p'].B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: Coeq_ind_type
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
p': DHom p (Coeq_ind_inv h).2 (Coeq_ind_inv k).2
h $== k
      snapply Coeq_ind.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: Coeq_ind_type
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
p': DHom p (Coeq_ind_inv h).2 (Coeq_ind_inv k).2
forall a : A,
(fun w : Coeq f g => h w $-> k w) (coeq a)
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: Coeq_ind_type
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
p': DHom p (Coeq_ind_inv h).2 (Coeq_ind_inv k).2
forall b : B,
transport (fun w : Coeq f g => h w $-> k w) (cglue b)
  (?coeq' (f b)) = ?coeq' (g b)
      1: exact p.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: Coeq_ind_type
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
p': DHom p (Coeq_ind_inv h).2 (Coeq_ind_inv k).2
forall b : B,
transport (fun w : Coeq f g => h w $-> k w) (cglue b)
  (p (f b)) = p (g b)
      intros b; specialize (p' b).B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: Coeq_ind_type
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
b: B
p': ap (transport P (cglue b)) (p (f b)) @
(Coeq_ind_inv k).2 b =
(Coeq_ind_inv h).2 b @ p (g b)
transport (fun w : Coeq f g => h w $-> k w) (cglue b)
  (p (f b)) = p (g b)
      lhs napply transport_paths_FlFr_D.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: Coeq_ind_type
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
b: B
p': ap (transport P (cglue b)) (p (f b)) @
(Coeq_ind_inv k).2 b =
(Coeq_ind_inv h).2 b @ p (g b)
((apD h (cglue b))^ @
 ap (transport P (cglue b)) (p (f b))) @
apD k (cglue b) = p (g b)
      lhs napply concat_pp_p.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: Coeq_ind_type
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
b: B
p': ap (transport P (cglue b)) (p (f b)) @
(Coeq_ind_inv k).2 b =
(Coeq_ind_inv h).2 b @ p (g b)
(apD h (cglue b))^ @
(ap (transport P (cglue b)) (p (f b)) @
 apD k (cglue b)) = p (g b)
      lhs napply (whiskerL _ p').B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: Coeq_ind_type
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
b: B
p': ap (transport P (cglue b)) (p (f b)) @
(Coeq_ind_inv k).2 b =
(Coeq_ind_inv h).2 b @ p (g b)
(apD h (cglue b))^ @ ((Coeq_ind_inv h).2 b @ p (g b)) =
p (g b)
      lhs napply concat_p_pp.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: Coeq_ind_type
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
b: B
p': ap (transport P (cglue b)) (p (f b)) @
(Coeq_ind_inv k).2 b =
(Coeq_ind_inv h).2 b @ p (g b)
((apD h (cglue b))^ @ apD h (cglue b)) @ p (g b) =
p (g b)
      lhs napply (whiskerR (concat_Vp _)).B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: Coeq_ind_type
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
b: B
p': ap (transport P (cglue b)) (p (f b)) @
(Coeq_ind_inv k).2 b =
(Coeq_ind_inv h).2 b @ p (g b)
1 @ p (g b) = p (g b)
      napply concat_1p.
  Defined.

  Definition equiv_0gpd_Coeq_ind
    : Build_ZeroGpd Coeq_ind_type _ _ _
      $<~> Build_ZeroGpd (sig Coeq_ind_data) _ _ _.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
{|
  carrier := Coeq_ind_type;
  isgraph_carrier := isgraph_forall (Coeq f g) P;
  is01cat_carrier := is01cat_forall (Coeq f g) P;
  is0gpd_carrier := is0gpd_forall (Coeq f g) P
|} $<~>
{|
  carrier := {x : _ & Coeq_ind_data x};
  isgraph_carrier := isgraph_total Coeq_ind_data;
  is01cat_carrier := is01cat_total Coeq_ind_data;
  is0gpd_carrier := is0gpd_total Coeq_ind_data
|}
  Proof.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
{|
  carrier := Coeq_ind_type;
  isgraph_carrier := isgraph_forall (Coeq f g) P;
  is01cat_carrier := is01cat_forall (Coeq f g) P;
  is0gpd_carrier := is0gpd_forall (Coeq f g) P
|} $<~>
{|
  carrier := {x : _ & Coeq_ind_data x};
  isgraph_carrier := isgraph_total Coeq_ind_data;
  is01cat_carrier := is01cat_total Coeq_ind_data;
  is0gpd_carrier := is0gpd_total Coeq_ind_data
|}
    snapply Build_CatEquiv.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
{|
  carrier := Coeq_ind_type;
  isgraph_carrier := isgraph_forall (Coeq f g) P;
  is01cat_carrier := is01cat_forall (Coeq f g) P;
  is0gpd_carrier := is0gpd_forall (Coeq f g) P
|} $->
{|
  carrier := {x : _ & Coeq_ind_data x};
  isgraph_carrier := isgraph_total Coeq_ind_data;
  is01cat_carrier := is01cat_total Coeq_ind_data;
  is0gpd_carrier := is0gpd_total Coeq_ind_data
|}
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
CatIsEquiv ?f
    1: rapply Build_Fun01.B, A: Type
f, g: B -> A
P: Coeq f g -> Type
CatIsEquiv
  {|
    fun01_F := Coeq_ind_inv;
    fun01_is0functor := is0functor_Coeq_ind_inv
  |}
    rapply isequiv_0gpd_issurjinj.
  Defined.

End UnivProp.

(** Here we prove that the 0-groupoid universal property established in the previous section is natural with respect to [functor_coeq]. More precisely, we show that [Coeq_ind_inv] commutes with precomposition with [k] and [functor_coeq h k p q]. *)
Section UnivPropNat.
  Context {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)
    (P : Coeq f' g' -> Type).

  Local Open Scope dpath_scope.

  (** We recall these instances to allow Coq to infer the same 0-groupoid structures as in the previous section. *)
  Local Existing Instances isgraph_total | 1.
  Local Existing Instances isgraph_paths | 2.
  Local Existing Instances isdgraph_Coeq_ind_data.

  (** Help Coq find the same graph structure for the sigma-groupoid of [Coeq_ind_data] when precomposing with [functor_coeq]. *)
  Local Instance isgraph_Coeq_ind_data_total
    : IsGraph (sig (Coeq_ind_data f g (P o 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
P: Coeq f' g' -> Type
IsGraph
  {x : _ &
  Coeq_ind_data f g (P o functor_coeq h k p q) x}
  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
P: Coeq f' g' -> Type
IsGraph
  {x : _ &
  Coeq_ind_data f g (P o functor_coeq h k p q) x}
    rapply isgraph_total.
  Defined.

  (** Given a map out of [A'] that coequalizes the parallel pair [f'] and [g'], we construct a map out of [A] that coequalizes [f] and [g]. Precomposing with [k] yields a dependent map [forall a : A, P (coeq (k a))], and [functor_coeq_beta_cglue] gives us a way to relate the paths. *)
  Definition functor_Coeq_ind_data
    : sig (Coeq_ind_data f' g' P)
      -> sig (Coeq_ind_data f g (P o 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
P: Coeq f' g' -> Type
{x : _ & Coeq_ind_data f' g' P x} ->
{x : _ &
Coeq_ind_data f g (P o functor_coeq h k p q) x}
  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
P: Coeq f' g' -> Type
{x : _ & Coeq_ind_data f' g' P x} ->
{x : _ &
Coeq_ind_data f g (P o functor_coeq h k p q) x}
    intros [m r].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
P: Coeq f' g' -> Type
m: forall a : A', P (coeq a)
r: Coeq_ind_data f' g' P m
{x : _ &
Coeq_ind_data f g
  (fun x : Coeq f g => P (functor_coeq h k p q x)) x}
    exists (m o k).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
P: Coeq f' g' -> Type
m: forall a : A', P (coeq a)
r: Coeq_ind_data f' g' P m
Coeq_ind_data f g
  (fun x : Coeq f g => P (functor_coeq h k p q x))
  (fun x : A => m (k x))
    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
P: Coeq f' g' -> Type
m: forall a : A', P (coeq a)
r: Coeq_ind_data f' g' P m
b: B
DPath (fun x : Coeq f g => P (functor_coeq h k p q x))
  (cglue b) (m (k (f b))) (m (k (g b)))
    unfold Coeq_ind_data in r.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
P: Coeq f' g' -> Type
m: forall a : A', P (coeq a)
r: forall b : B',
DPath P (cglue b) (m (f' b)) (m (g' b))
b: B
DPath (fun x : Coeq f g => P (functor_coeq h k p q x))
  (cglue b) (m (k (f b))) (m (k (g b)))
    apply (dp_compose' _ _ (functor_coeq_beta_cglue h k p 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
P: Coeq f' g' -> Type
m: forall a : A', P (coeq a)
r: forall b : B',
DPath P (cglue b) (m (f' b)) (m (g' b))
b: B
DPath P
  ((ap coeq (p b) @ cglue (h b)) @ ap coeq (q b)^)
  (m (k (f b))) (m (k (g b)))
    nrefine (_ @Dp r (h b) @Dp _).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
P: Coeq f' g' -> Type
m: forall a : A', P (coeq a)
r: forall b : B',
DPath P (cglue b) (m (f' b)) (m (g' b))
b: B
DPath P (ap coeq (p b)) (m (k (f b))) (m (f' (h 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
P: Coeq f' g' -> Type
m: forall a : A', P (coeq a)
r: forall b : B',
DPath P (cglue b) (m (f' b)) (m (g' b))
b: B
DPath P (ap coeq (q b)^) (m (g' (h b))) (m (k (g b)))
    1: exact (dp_compose coeq P (p b) (apD m (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
P: Coeq f' g' -> Type
m: forall a : A', P (coeq a)
r: forall b : B',
DPath P (cglue b) (m (f' b)) (m (g' b))
b: B
DPath P (ap coeq (q b)^) (m (g' (h b))) (m (k (g b)))
    exact (dp_compose coeq P (q b)^ (apD m (q b)^)).
  Defined.

  (** A helper lemma for proving functoriality of [functor_Coeq_ind_data]. This is the action of [Coeq_ind _ _ _ o functor_coeq h k p q] on the path [cglue b]. *)
  Local Lemma Coeq_ind_functor_coeq_beta_cglue {b : B}
    {m : forall a' : A', P (coeq a')}
    {r : forall b' : B', DPath P (cglue b') (m (f' b')) (m (g' b'))}
    : apD (fun x => Coeq_ind P m r (functor_coeq h k p q x)) (cglue b)
      = (dp_compose' (functor_coeq h k p q) P (functor_coeq_beta_cglue h k p q b))^-1
          ((dp_compose coeq P (p b) (apD m (p b)) @Dp r (h b)) @Dp
          dp_compose coeq P (q b)^ (apD m (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
P: Coeq f' g' -> Type
b: B
m: forall a' : A', P (coeq a')
r: forall b' : B',
DPath P (cglue b') (m (f' b')) (m (g' b'))
apD
  (fun x : Coeq f g =>
   Coeq_ind P m r (functor_coeq h k p q x)) (cglue b) =
(dp_compose' (functor_coeq h k p q) P
   (functor_coeq_beta_cglue h k p q b))^-1
  ((dp_compose coeq P (p b) (apD m (p b)) @Dp r (h b)) @Dp
   dp_compose coeq P (q b)^ (apD m (q b)^))
  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
P: Coeq f' g' -> Type
b: B
m: forall a' : A', P (coeq a')
r: forall b' : B',
DPath P (cglue b') (m (f' b')) (m (g' b'))
apD
  (fun x : Coeq f g =>
   Coeq_ind P m r (functor_coeq h k p q x)) (cglue b) =
(dp_compose' (functor_coeq h k p q) P
   (functor_coeq_beta_cglue h k p q b))^-1
  ((dp_compose coeq P (p b) (apD m (p b)) @Dp r (h b)) @Dp
   dp_compose coeq P (q b)^ (apD m (q b)^))
    nrefine (ap _ _ @ (dp_apD_compose' _ _ _ (Coeq_ind P m r))^)^.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
P: Coeq f' g' -> Type
b: B
m: forall a' : A', P (coeq a')
r: forall b' : B',
DPath P (cglue b') (m (f' b')) (m (g' b'))
(dp_compose coeq P (p b) (apD m (p b)) @Dp r (h b)) @Dp
dp_compose coeq P (q b)^ (apD m (q b)^) =
apD (Coeq_ind P m r)
  ((ap coeq (p b) @ cglue (h b)) @ ap coeq (q b)^)
    lhs napply (dp_whiskerL _ (dp_apD_compose_inv coeq P (Coeq_ind P m r))^).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
P: Coeq f' g' -> Type
b: B
m: forall a' : A', P (coeq a')
r: forall b' : B',
DPath P (cglue b') (m (f' b')) (m (g' b'))
(dp_compose coeq P (p b) (apD m (p b)) @Dp r (h b)) @Dp
apD (Coeq_ind P m r) (ap coeq (q b)^) =
apD (Coeq_ind P m r)
  ((ap coeq (p b) @ cglue (h b)) @ ap coeq (q b)^)
    lhs napply (dp_whiskerR _ (dp_whiskerR _ (dp_apD_compose_inv coeq 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
P: Coeq f' g' -> Type
b: B
m: forall a' : A', P (coeq a')
r: forall b' : B',
DPath P (cglue b') (m (f' b')) (m (g' b'))
(apD (Coeq_ind P m r) (ap coeq (p b)) @Dp r (h b)) @Dp
apD (Coeq_ind P m r) (ap coeq (q b)^) =
apD (Coeq_ind P m r)
  ((ap coeq (p b) @ cglue (h b)) @ ap coeq (q b)^)
    lhs napply (dp_whiskerR _ (dp_whiskerL _ (Coeq_ind_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
P: Coeq f' g' -> Type
b: B
m: forall a' : A', P (coeq a')
r: forall b' : B',
DPath P (cglue b') (m (f' b')) (m (g' b'))
(apD (Coeq_ind P m r) (ap coeq (p b)) @Dp
 apD (Coeq_ind P m r) (cglue (h b))) @Dp
apD (Coeq_ind P m r) (ap coeq (q b)^) =
apD (Coeq_ind P m r)
  ((ap coeq (p b) @ cglue (h b)) @ ap coeq (q b)^)
    lhs napply (dp_whiskerR _ (dp_apD_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
P: Coeq f' g' -> Type
b: B
m: forall a' : A', P (coeq a')
r: forall b' : B',
DPath P (cglue b') (m (f' b')) (m (g' b'))
apD (Coeq_ind P m r) (ap coeq (p b) @ cglue (h b)) @Dp
apD (Coeq_ind P m r) (ap coeq (q b)^) =
apD (Coeq_ind P m r)
  ((ap coeq (p b) @ cglue (h b)) @ ap coeq (q b)^)
    exact (dp_apD_pp _ _ _ _ _)^.
  Defined.

  Local Instance is0functor_functor_Coeq_ind_data
    : Is0Functor functor_Coeq_ind_data.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
P: Coeq f' g' -> Type
Is0Functor functor_Coeq_ind_data
  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
P: Coeq f' g' -> Type
Is0Functor functor_Coeq_ind_data
    napply Build_Is0Functor.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
P: Coeq f' g' -> Type
forall a b : {x : _ & Coeq_ind_data f' g' P x},
(a $-> b) ->
functor_Coeq_ind_data a $-> functor_Coeq_ind_data b
    intros [m r] [n s] [u 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
P: Coeq f' g' -> Type
m: forall a : A', P (coeq a)
r: Coeq_ind_data f' g' P m
n: forall a : A', P (coeq a)
s: Coeq_ind_data f' g' P n
u: m $-> n
v: DHom u r s
functor_Coeq_ind_data (m; r) $->
functor_Coeq_ind_data (n; s)
    exists (u o k).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
P: Coeq f' g' -> Type
m: forall a : A', P (coeq a)
r: Coeq_ind_data f' g' P m
n: forall a : A', P (coeq a)
s: Coeq_ind_data f' g' P n
u: m $-> n
v: DHom u r s
DHom (fun x : A => u (k x))
  (functor_Coeq_ind_data (m; r)).2
  (functor_Coeq_ind_data (n; s)).2
    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
P: Coeq f' g' -> Type
m: forall a : A', P (coeq a)
r: Coeq_ind_data f' g' P m
n: forall a : A', P (coeq a)
s: Coeq_ind_data f' g' P n
u: m $-> n
v: DHom u r s
b: B
ap
  (transport
     (fun x : Coeq f g => P (functor_coeq h k p q x))
     (cglue b)) (u (k (f b))) @
(functor_Coeq_ind_data (n; s)).2 b =
(functor_Coeq_ind_data (m; r)).2 b @ u (k (g b))
    lhs napply (whiskerL _ Coeq_ind_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
P: Coeq f' g' -> Type
m: forall a : A', P (coeq a)
r: Coeq_ind_data f' g' P m
n: forall a : A', P (coeq a)
s: Coeq_ind_data f' g' P n
u: m $-> n
v: DHom u r s
b: B
ap
  (transport
     (fun x : Coeq f g => P (functor_coeq h k p q x))
     (cglue b)) (u (k (f b))) @
apD
  (fun x : Coeq f g =>
   Coeq_ind P n s (functor_coeq h k p q x)) (cglue b) =
(functor_Coeq_ind_data (m; r)).2 b @ u (k (g b))
    rhs napply (whiskerR Coeq_ind_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
P: Coeq f' g' -> Type
m: forall a : A', P (coeq a)
r: Coeq_ind_data f' g' P m
n: forall a : A', P (coeq a)
s: Coeq_ind_data f' g' P n
u: m $-> n
v: DHom u r s
b: B
ap
  (transport
     (fun x : Coeq f g => P (functor_coeq h k p q x))
     (cglue b)) (u (k (f b))) @
apD
  (fun x : Coeq f g =>
   Coeq_ind P n s (functor_coeq h k p q x)) (cglue b) =
apD
  (fun x : Coeq f g =>
   Coeq_ind P m r (functor_coeq h k p q x)) (cglue b) @
u (k (g b))
    napply moveL_Mp.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
P: Coeq f' g' -> Type
m: forall a : A', P (coeq a)
r: Coeq_ind_data f' g' P m
n: forall a : A', P (coeq a)
s: Coeq_ind_data f' g' P n
u: m $-> n
v: DHom u r s
b: B
(apD
   (fun x : Coeq f g =>
    Coeq_ind P m r (functor_coeq h k p q x)) (cglue b))^ @
(ap
   (transport
      (fun x : Coeq f g => P (functor_coeq h k p q x))
      (cglue b)) (u (k (f b))) @
 apD
   (fun x : Coeq f g =>
    Coeq_ind P n s (functor_coeq h k p q x)) (cglue b)) =
u (k (g b))
    lhs napply 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
P: Coeq f' g' -> Type
m: forall a : A', P (coeq a)
r: Coeq_ind_data f' g' P m
n: forall a : A', P (coeq a)
s: Coeq_ind_data f' g' P n
u: m $-> n
v: DHom u r s
b: B
((apD
    (fun x : Coeq f g =>
     Coeq_ind P m r (functor_coeq h k p q x))
    (cglue b))^ @
 ap
   (transport
      (fun x : Coeq f g => P (functor_coeq h k p q x))
      (cglue b)) (u (k (f b)))) @
apD
  (fun x : Coeq f g =>
   Coeq_ind P n s (functor_coeq h k p q x)) (cglue b) =
u (k (g b))
    lhs nrefine (transport_paths_FlFr_D (cglue b) (Coeq_ind_homotopy P u 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
P: Coeq f' g' -> Type
m: forall a : A', P (coeq a)
r: Coeq_ind_data f' g' P m
n: forall a : A', P (coeq a)
s: Coeq_ind_data f' g' P n
u: m $-> n
v: DHom u r s
b: B
transport
  (fun x : Coeq f g =>
   Coeq_ind P m r (functor_coeq h k p q x) =
   Coeq_ind P n s (functor_coeq h k p q x)) (cglue b)
  (Coeq_ind_homotopy P u v
     (functor_coeq h k p q (coeq (f b)))) =
u (k (g b))
    apply (ds_dp (Coeq_ind P m r o _) (Coeq_ind P n s o _) _ _ _).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
P: Coeq f' g' -> Type
m: forall a : A', P (coeq a)
r: Coeq_ind_data f' g' P m
n: forall a : A', P (coeq a)
s: Coeq_ind_data f' g' P n
u: m $-> n
v: DHom u r s
b: B
DPathSquare
  (fun x : Coeq f g => P (functor_coeq h k p q x))
  (PathSquare.sq_refl_h (cglue b))
  (apD
     (fun x : Coeq f g =>
      Coeq_ind P m r (functor_coeq h k p q x))
     (cglue b))
  (apD
     (fun x : Coeq f g =>
      Coeq_ind P n s (functor_coeq h k p q x))
     (cglue b))
  (Coeq_ind_homotopy P u v
     (functor_coeq h k p q (coeq (f b))))
  (u (k (g b)))
    exact (dp_apD_nat (Coeq_ind_homotopy P u v o _) (cglue b)).
  Defined.

  (** Recall the domain of this functor is the type of dependent maps [forall z : Coeq f' g', P z]. By precomposing with [functor_coeq h k p q : Coeq f g -> Coeq f' g'] we get a dependent map [forall z : Coeq f g, (P (functor_coeq h k p q z))]. *)
  Definition functor_Coeq_ind_type
    : Coeq_ind_type f' g' P -> Coeq_ind_type f g (P o functor_coeq h k p q)
    := fun x => x o functor_coeq h k p q.

  Local Instance is0functor_functor_Coeq_ind_type
    : Is0Functor functor_Coeq_ind_type.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
P: Coeq f' g' -> Type
Is0Functor functor_Coeq_ind_type
  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
P: Coeq f' g' -> Type
Is0Functor functor_Coeq_ind_type
    napply Build_Is0Functor.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
P: Coeq f' g' -> Type
forall a b : Coeq_ind_type f' g' P,
(a $-> b) ->
functor_Coeq_ind_type a $-> functor_Coeq_ind_type b
    intros m n r.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
P: Coeq f' g' -> Type
m, n: Coeq_ind_type f' g' P
r: m $-> n
functor_Coeq_ind_type m $-> functor_Coeq_ind_type n
    exact (r o functor_coeq h k p q).
  Defined.

  (** We now have two different ways of mapping from [Coeq_ind_type f' g' P] to [sig (Coeq_ind_data f g (P o functor_coeq h k p q))]. Here we construct a transformation between these two maps.
<<
  Coeq_ind_type f' g' P ---------functor_Coeq_ind_type---> Coeq_ind_type f g (P o functor_coeq h k p q)
        |                                                                   |
        |                                                                   |
  Coeq_ind_inv f' g' P                                      Coeq_ind_inv f g (P o functor_coeq h k p q)
        |                                                                   |
        |                                                                   |
        V                                                                   V
  sig (Coeq_ind_data f' g' P) ---functor_Coeq_ind_data---> sig (Coeq_ind_data f g (P o functor_coeq h k p q))
>>
  *)
  Definition Coeq_ind_inv_nat
    : Coeq_ind_inv f g (P o functor_coeq h k p q) o functor_Coeq_ind_type
      $=> functor_Coeq_ind_data o (Coeq_ind_inv f' g' 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
P: Coeq f' g' -> Type
Coeq_ind_inv f g (P o functor_coeq h k p q)
o functor_Coeq_ind_type $=>
functor_Coeq_ind_data o Coeq_ind_inv f' g' P
  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
P: Coeq f' g' -> Type
Coeq_ind_inv f g (P o functor_coeq h k p q)
o functor_Coeq_ind_type $=>
functor_Coeq_ind_data o Coeq_ind_inv f' g' P
    intros m.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
P: Coeq f' g' -> Type
m: Coeq_ind_type f' g' P
Coeq_ind_inv f g
  (fun x : Coeq f g => P (functor_coeq h k p q x))
  (functor_Coeq_ind_type m) $->
functor_Coeq_ind_data (Coeq_ind_inv f' g' P m)
    exists (fun _ => idpath).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
P: Coeq f' g' -> Type
m: Coeq_ind_type f' g' P
DHom (fun H : A => 1%path)
  (Coeq_ind_inv f g
     (fun x : Coeq f g => P (functor_coeq h k p q x))
     (functor_Coeq_ind_type m)).2
  (functor_Coeq_ind_data (Coeq_ind_inv f' g' P m)).2
    intros b; simpl.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
P: Coeq f' g' -> Type
m: Coeq_ind_type f' g' P
b: B
1 @
(dp_compose' (functor_coeq h k p q) P
   (functor_coeq_beta_cglue h k p q b))^-1
  ((dp_compose coeq P (p b)
      (apD (fun x : A' => m (coeq x)) (p b)) @Dp
    apD m (cglue (h b))) @Dp
   dp_compose coeq P (q b)^
     (apD (fun x : A' => m (coeq x)) (q b)^)) =
apD (functor_Coeq_ind_type m) (cglue b) @ 1
    lhs napply concat_1p; rhs napply concat_p1.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
P: Coeq f' g' -> Type
m: Coeq_ind_type f' g' P
b: B
(dp_compose' (functor_coeq h k p q) P
   (functor_coeq_beta_cglue h k p q b))^-1
  ((dp_compose coeq P (p b)
      (apD (fun x : A' => m (coeq x)) (p b)) @Dp
    apD m (cglue (h b))) @Dp
   dp_compose coeq P (q b)^
     (apD (fun x : A' => m (coeq x)) (q b)^)) =
apD (functor_Coeq_ind_type m) (cglue b)
    rhs napply (dp_apD_compose' _ _ (functor_coeq_beta_cglue h k p 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
P: Coeq f' g' -> Type
m: Coeq_ind_type f' g' P
b: B
(dp_compose' (functor_coeq h k p q) P
   (functor_coeq_beta_cglue h k p q b))^-1
  ((dp_compose coeq P (p b)
      (apD (fun x : A' => m (coeq x)) (p b)) @Dp
    apD m (cglue (h b))) @Dp
   dp_compose coeq P (q b)^
     (apD (fun x : A' => m (coeq x)) (q b)^)) =
(dp_compose' (functor_coeq h k p q) P
   (functor_coeq_beta_cglue h k p q b))^-1
  (apD m
     ((ap coeq (p b) @ cglue (h b)) @ ap coeq (q b)^))
    napply ap.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
P: Coeq f' g' -> Type
m: Coeq_ind_type f' g' P
b: B
(dp_compose coeq P (p b)
   (apD (fun x : A' => m (coeq x)) (p b)) @Dp
 apD m (cglue (h b))) @Dp
dp_compose coeq P (q b)^
  (apD (fun x : A' => m (coeq x)) (q b)^) =
apD m ((ap coeq (p b) @ cglue (h b)) @ ap coeq (q b)^)
    nrefine (_ @ (dp_apD_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
P: Coeq f' g' -> Type
m: Coeq_ind_type f' g' P
b: B
(dp_compose coeq P (p b)
   (apD (fun x : A' => m (coeq x)) (p b)) @Dp
 apD m (cglue (h b))) @Dp
dp_compose coeq P (q b)^
  (apD (fun x : A' => m (coeq x)) (q b)^) =
apD m (ap coeq (p b) @ cglue (h b)) @Dp
apD m (ap coeq (q b)^)
    rhs napply (dp_whiskerR _ (dp_apD_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
P: Coeq f' g' -> Type
m: Coeq_ind_type f' g' P
b: B
(dp_compose coeq P (p b)
   (apD (fun x : A' => m (coeq x)) (p b)) @Dp
 apD m (cglue (h b))) @Dp
dp_compose coeq P (q b)^
  (apD (fun x : A' => m (coeq x)) (q b)^) =
(apD m (ap coeq (p b)) @Dp apD m (cglue (h b))) @Dp
apD m (ap coeq (q b)^)
    lhs napply (dp_whiskerL _ (dp_apD_compose_inv _ _ _)^).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
P: Coeq f' g' -> Type
m: Coeq_ind_type f' g' P
b: B
(dp_compose coeq P (p b)
   (apD (fun x : A' => m (coeq x)) (p b)) @Dp
 apD m (cglue (h b))) @Dp apD m (ap coeq (q b)^) =
(apD m (ap coeq (p b)) @Dp apD m (cglue (h b))) @Dp
apD m (ap coeq (q b)^)
    exact (dp_whiskerR _ (dp_whiskerR _ (dp_apD_compose_inv _ _ _)^)).
  Defined.

End UnivPropNat.