DisplayedEquiv.v

Require Import Basics.Overture.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Basics.Tactics.
Require Import Basics.Equivalences.
Require Import Types.Sigma.
Require Import WildCat.Core.
Require Import WildCat.Displayed.
Require Import WildCat.Equiv.

(** Equivalences in displayed wild categories *)
Class DHasEquivs {A : Type} `{HasEquivs A}
  (D : A -> Type) `{!IsDGraph D, !IsD2Graph D, !IsD01Cat D, !IsD1Cat D} :=
{
  DCatEquiv : forall {a b : A}, (a $<~> b) -> D a -> D b -> Type;
  DCatIsEquiv : forall {a b : A} {f : a $-> b} {fe : CatIsEquiv f} {a'} {b'},
    DHom f a' b' -> Type;
  dcate_fun : forall {a b : A} {f : a $<~> b} {a'} {b'},
    DCatEquiv f a' b' -> DHom f a' b';
  dcate_isequiv : forall {a b : A} {f : a $<~> b} {a'} {b'}
    (f' : DCatEquiv f a' b'), DCatIsEquiv (dcate_fun f');
  dcate_buildequiv : forall {a b : A} {f : a $-> b} `{!CatIsEquiv f} {a'} {b'}
    (f' : DHom f a' b') {fe' : DCatIsEquiv f'},
    DCatEquiv (Build_CatEquiv f) a' b';
  dcate_buildequiv_fun : forall {a b : A} {f : a $-> b} `{!CatIsEquiv f}
    {a'} {b'} (f' : DHom f a' b') {fe' : DCatIsEquiv f'},
    DGpdHom (cate_buildequiv_fun f)
    (dcate_fun (dcate_buildequiv f' (fe':=fe'))) f';
  dcate_inv' : forall {a b : A} {f : a $<~> b} {a'} {b'} (f' : DCatEquiv f a' b'),
    DHom (cate_inv' _ _ f) b' a';
  dcate_issect' : forall {a b : A} {f : a $<~> b} {a'} {b'} (f' : DCatEquiv f a' b'),
    DGpdHom (cate_issect' _ _ f) (dcate_inv' f' $o' dcate_fun f') (DId a');
  dcate_isretr' : forall {a b : A} {f : a $<~> b} {a'} {b'} (f' : DCatEquiv f a' b'),
    DGpdHom (cate_isretr' _ _ f) (dcate_fun f' $o' dcate_inv' f') (DId b');
  dcatie_adjointify : forall {a b : A} {f : a $-> b} {g : b $-> a}
    {r : f $o g $== Id b} {s : g $o f $== Id a} {a'} {b'} (f' : DHom f a' b')
    (g' : DHom g b' a') (r' : DGpdHom r (f' $o' g') (DId b'))
    (s' : DGpdHom s (g' $o' f') (DId a')),
    @DCatIsEquiv _ _ _ (catie_adjointify f g r s) _ _ f';
}.

(** Being an equivalence is a typeclass. *)
Existing Class DCatIsEquiv.
Existing Instance dcate_isequiv.

Coercion dcate_fun : DCatEquiv >-> DHom.

Definition Build_DCatEquiv {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {f : a $-> b} `{!CatIsEquiv f} {a' : D a} {b' : D b}
  (f' : DHom f a' b') {fe' : DCatIsEquiv f'}
  : DCatEquiv (Build_CatEquiv f) a' b'
  := dcate_buildequiv f' (fe':=fe').

(** Construct [DCatEquiv] via adjointify. *)
Definition dcate_adjointify {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {f : a $-> b} {g : b $-> a}
  {r : f $o g $== Id b} {s : g $o f $== Id a} {a'} {b'}
  (f' : DHom f a' b') (g' : DHom g b' a') (r' : DHom r (f' $o' g') (DId b'))
  (s' : DHom s (g' $o' f') (DId a'))
  : DCatEquiv (cate_adjointify f g r s) a' b'
  := Build_DCatEquiv f' (fe':=dcatie_adjointify f' g' r' s').

(** Construct the entire inverse equivalence *)
Definition dcate_inv {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {f : a $<~> b} {a' : D a} {b' : D b} (f' : DCatEquiv f a' b')
  : DCatEquiv (f^-1$) b' a'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DCatEquiv f^-1$ b' a'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DCatEquiv f^-1$ b' a'
  snapply dcate_adjointify.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DHom (cate_inv' a b f) b' a'
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DHom f a' b'
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DHom (cate_issect' a b f) (?f' $o' ?g') (DId a')
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DHom (cate_isretr' a b f) (?g' $o' ?f') (DId b')
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DHom (cate_inv' a b f) b' a' exact (dcate_inv' f').
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DHom f a' b' exact f'.
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DHom (cate_issect' a b f) (dcate_inv' f' $o' f')
  (DId a') exact (dcate_issect' f').
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DHom (cate_isretr' a b f) (f' $o' dcate_inv' f')
  (DId b') exact (dcate_isretr' f').
Defined.

Notation "f ^-1$'" := (dcate_inv f).

(** Witness that [f'] is a section of [dcate_inv f'] in addition to [dcate_inv' f']. *)
Definition dcate_issect {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {f : a $<~> b} {a' : D a} {b' : D b} (f' : DCatEquiv f a' b')
  : DGpdHom (cate_issect f) (dcate_fun f'^-1$' $o' f') (DId a').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DGpdHom (cate_issect f) (f'^-1$' $o' f') (DId a')
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DGpdHom (cate_issect f) (f'^-1$' $o' f') (DId a')
  refine (_ $@' dcate_issect' f').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DGpdHom
  (cate_buildequiv_fun' b a (cate_inv' a b f)
     (catie_adjointify (cate_inv' a b f) f
        (cate_issect' a b f) (cate_isretr' a b f)) $@R
   f) (f'^-1$' $o' f') (dcate_inv' f' $o' f')
  refine (_ $@R' (dcate_fun f')).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DHom
  (cate_buildequiv_fun' b a (cate_inv' a b f)
     (catie_adjointify (cate_inv' a b f) f
        (cate_issect' a b f) (cate_isretr' a b f)))
  f'^-1$' (dcate_inv' f')
  apply dcate_buildequiv_fun.
Defined.

(** Witness that [f'] is a retraction of [dcate_inv f'] in addition to [dcate_inv' f']. *)
Definition dcate_isretr {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {f : a $<~> b} {a' : D a} {b' : D b} (f' : DCatEquiv f a' b')
  : DGpdHom (cate_isretr f) (dcate_fun f' $o' f'^-1$') (DId b').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DGpdHom (cate_isretr f) (f' $o' f'^-1$') (DId b')
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DGpdHom (cate_isretr f) (f' $o' f'^-1$') (DId b')
  refine (_ $@' dcate_isretr' f').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DGpdHom
  (cate_buildequiv_fun' a b (cate_inv' b a f)
     (catie_adjointify (cate_inv' b a f) f
        (cate_issect' b a f) (cate_isretr' b a f)) $@R
   f) (f' $o' f'^-1$') (f' $o' dcate_inv' f')
  refine (dcate_fun f' $@L' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DHom
  (cate_buildequiv_fun' a b (cate_inv' b a f)
     (catie_adjointify (cate_inv' b a f) f
        (cate_issect' b a f) (cate_isretr' b a f)))
  f'^-1$' (dcate_inv' f')
  apply dcate_buildequiv_fun.
Defined.

(** If [g'] is a section of an equivalence, then it is the inverse. *)
Definition dcate_inverse_sect {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {f : a $<~> b} {g : b $-> a} {p : f $o g $== Id b}
  {a' : D a} {b' : D b} (f' : DCatEquiv f a' b') (g' : DHom g b' a')
  (p' : DGpdHom p (dcate_fun f' $o' g') (DId b'))
  : DGpdHom (cate_inverse_sect f g p) (dcate_fun f'^-1$') g'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
g: b $-> a
p: f $o g $== Id b
a': D a
b': D b
f': DCatEquiv f a' b'
g': DHom g b' a'
p': DGpdHom p (f' $o' g') (DId b')
DGpdHom (cate_inverse_sect f g p) f'^-1$' g'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
g: b $-> a
p: f $o g $== Id b
a': D a
b': D b
f': DCatEquiv f a' b'
g': DHom g b' a'
p': DGpdHom p (f' $o' g') (DId b')
DGpdHom (cate_inverse_sect f g p) f'^-1$' g'
  refine ((dcat_idr _)^$' $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
g: b $-> a
p: f $o g $== Id b
a': D a
b': D b
f': DCatEquiv f a' b'
g': DHom g b' a'
p': DGpdHom p (f' $o' g') (DId b')
DGpdHom
  ((f^-1$ $@L p^$) $@
   (cat_assoc_opp g f f^-1$ $@
    ((cate_issect f $@R g) $@ cat_idl g)))
  (f'^-1$' $o' DId b') g'
  refine ((_ $@L' p'^$') $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
g: b $-> a
p: f $o g $== Id b
a': D a
b': D b
f': DCatEquiv f a' b'
g': DHom g b' a'
p': DGpdHom p (f' $o' g') (DId b')
IsD0Gpd (fun f : b $-> b => DHom f b' b')
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
g: b $-> a
p: f $o g $== Id b
a': D a
b': D b
f': DCatEquiv f a' b'
g': DHom g b' a'
p': DGpdHom p (f' $o' g') (DId b')
DGpdHom
  (cat_assoc_opp g f f^-1$ $@
   ((cate_issect f $@R g) $@ cat_idl g))
  (f'^-1$' $o' (f' $o' g')) g'
  1: exact isd0gpd_hom.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
g: b $-> a
p: f $o g $== Id b
a': D a
b': D b
f': DCatEquiv f a' b'
g': DHom g b' a'
p': DGpdHom p (f' $o' g') (DId b')
DGpdHom
  (cat_assoc_opp g f f^-1$ $@
   ((cate_issect f $@R g) $@ cat_idl g))
  (f'^-1$' $o' (f' $o' g')) g'
  refine (dcat_assoc_opp _ _ _ $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
g: b $-> a
p: f $o g $== Id b
a': D a
b': D b
f': DCatEquiv f a' b'
g': DHom g b' a'
p': DGpdHom p (f' $o' g') (DId b')
DGpdHom ((cate_issect f $@R g) $@ cat_idl g)
  (f'^-1$' $o' f' $o' g') g'
  refine (dcate_issect f' $@R' _ $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
g: b $-> a
p: f $o g $== Id b
a': D a
b': D b
f': DCatEquiv f a' b'
g': DHom g b' a'
p': DGpdHom p (f' $o' g') (DId b')
DGpdHom (cat_idl g) (DId a' $o' g') g'
  apply dcat_idl.
Defined.

(** If [g'] is a retraction of an equivalence, then it is the inverse. *)
Definition dcate_inverse_retr {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {f : a $<~> b} {g : b $-> a} {p : g $o f $== Id a}
  {a' : D a} {b' : D b} (f' : DCatEquiv f a' b') (g' : DHom g b' a')
  (p' : DGpdHom p (g' $o' f') (DId a'))
  : DGpdHom (cate_inverse_retr f g p) (dcate_fun f'^-1$') g'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
g: b $-> a
p: g $o f $== Id a
a': D a
b': D b
f': DCatEquiv f a' b'
g': DHom g b' a'
p': DGpdHom p (g' $o' f') (DId a')
DGpdHom (cate_inverse_retr f g p) f'^-1$' g'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
g: b $-> a
p: g $o f $== Id a
a': D a
b': D b
f': DCatEquiv f a' b'
g': DHom g b' a'
p': DGpdHom p (g' $o' f') (DId a')
DGpdHom (cate_inverse_retr f g p) f'^-1$' g'
  refine ((dcat_idl _)^$' $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
g: b $-> a
p: g $o f $== Id a
a': D a
b': D b
f': DCatEquiv f a' b'
g': DHom g b' a'
p': DGpdHom p (g' $o' f') (DId a')
DGpdHom
  ((f^-1$ $@L p^$) $@
   (cat_assoc_opp g f f^-1$ $@
    ((cate_issect f $@R g) $@ cat_idl g)))
  (DId a' $o' f'^-1$') g'
  refine ((p'^$' $@R' _) $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
g: b $-> a
p: g $o f $== Id a
a': D a
b': D b
f': DCatEquiv f a' b'
g': DHom g b' a'
p': DGpdHom p (g' $o' f') (DId a')
IsD0Gpd (fun f : a $-> a => DHom f a' a')
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
g: b $-> a
p: g $o f $== Id a
a': D a
b': D b
f': DCatEquiv f a' b'
g': DHom g b' a'
p': DGpdHom p (g' $o' f') (DId a')
DGpdHom
  (cat_assoc_opp g f f^-1$ $@
   ((cate_issect f $@R g) $@ cat_idl g))
  (g' $o' f' $o' f'^-1$') g'
  1: exact isd0gpd_hom.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
g: b $-> a
p: g $o f $== Id a
a': D a
b': D b
f': DCatEquiv f a' b'
g': DHom g b' a'
p': DGpdHom p (g' $o' f') (DId a')
DGpdHom
  (cat_assoc_opp g f f^-1$ $@
   ((cate_issect f $@R g) $@ cat_idl g))
  (g' $o' f' $o' f'^-1$') g'
  refine (dcat_assoc _ _ _ $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
g: b $-> a
p: g $o f $== Id a
a': D a
b': D b
f': DCatEquiv f a' b'
g': DHom g b' a'
p': DGpdHom p (g' $o' f') (DId a')
DGpdHom ((cate_issect f $@R g) $@ cat_idl g)
  (g' $o' (f' $o' f'^-1$')) g'
  refine (_ $@L' dcate_isretr f' $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
g: b $-> a
p: g $o f $== Id a
a': D a
b': D b
f': DCatEquiv f a' b'
g': DHom g b' a'
p': DGpdHom p (g' $o' f') (DId a')
DGpdHom (cat_idl g) (g' $o' DId b') g'
  apply dcat_idr.
Defined.

(** It follows that the inverse of the equivalence you get by adjointification is homotopic to the inverse [g'] provided. *)
Definition dcate_inv_adjointify {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {f : a $-> b} {g : b $-> a} {r : f $o g $== Id b}
  {s : g $o f $== Id a} {a' : D a} {b' : D b} (f' : DHom f a' b')
  (g' : DHom g b' a') (r' : DGpdHom r (f' $o' g') (DId b'))
  (s' : DGpdHom s (g' $o' f') (DId a'))
  : DGpdHom (cate_inv_adjointify f g r s)
    (dcate_fun (dcate_adjointify f' g' r' s')^-1$') g'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
g: b $-> a
r: f $o g $== Id b
s: g $o f $== Id a
a': D a
b': D b
f': DHom f a' b'
g': DHom g b' a'
r': DGpdHom r (f' $o' g') (DId b')
s': DGpdHom s (g' $o' f') (DId a')
DGpdHom (cate_inv_adjointify f g r s)
  (dcate_adjointify f' g' r' s')^-1$' g'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
g: b $-> a
r: f $o g $== Id b
s: g $o f $== Id a
a': D a
b': D b
f': DHom f a' b'
g': DHom g b' a'
r': DGpdHom r (f' $o' g') (DId b')
s': DGpdHom s (g' $o' f') (DId a')
DGpdHom (cate_inv_adjointify f g r s)
  (dcate_adjointify f' g' r' s')^-1$' g'
  apply dcate_inverse_sect.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
g: b $-> a
r: f $o g $== Id b
s: g $o f $== Id a
a': D a
b': D b
f': DHom f a' b'
g': DHom g b' a'
r': DGpdHom r (f' $o' g') (DId b')
s': DGpdHom s (g' $o' f') (DId a')
DGpdHom ((cate_buildequiv_fun f $@R g) $@ r)
  (dcate_adjointify f' g' r' s' $o' g') (DId b')
  exact ((dcate_buildequiv_fun f' $@R' _) $@' r').
Defined.

(** If the base category has equivalences and the displayed category has displayed equivalences, then the total category has equivalences. *)
Instance hasequivs_total {A} (D : A -> Type) `{DHasEquivs A D}
  : HasEquivs (sig D).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
HasEquivs {x : _ & D x}
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
HasEquivs {x : _ & D x}
  snapply Build_HasEquivs.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
{x : _ & D x} -> {x : _ & D x} -> Type
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall a b : {x : _ & D x}, (a $-> b) -> Type
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall a b : {x : _ & D x}, ?CatEquiv' a b -> a $-> b
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall (a b : {x : _ & D x}) 
(f : ?CatEquiv' a b),
?CatIsEquiv' a b (?cate_fun' a b f)
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall (a b : {x : _ & D x}) 
(f : a $-> b), ?CatIsEquiv' a b f -> ?CatEquiv' a b
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall (a b : {x : _ & D x}) 
(f : a $-> b) (fe : ?CatIsEquiv' a b f),
?cate_fun' a b (?cate_buildequiv' a b f fe) $== f
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall a b : {x : _ & D x}, ?CatEquiv' a b -> b $-> a
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall (a b : {x : _ & D x}) 
(f : ?CatEquiv' a b),
?cate_inv' a b f $o ?cate_fun' a b f $== Id a
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall (a b : {x : _ & D x}) 
(f : ?CatEquiv' a b),
?cate_fun' a b f $o ?cate_inv' a b f $== Id b
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall (a b : {x : _ & D x}) 
(f : a $-> b) (g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a -> ?CatIsEquiv' a b f
  1:{A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
{x : _ & D x} -> {x : _ & D x} -> Type intros [a a'] [b b'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a: A
a': D a
b: A
b': D b
Type exact {f : a $<~> b & DCatEquiv f a' b'}. }A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall a b : {x : _ & D x}, (a $-> b) -> Type
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall a b : {x : _ & D x},
(fun X : {x : _ & D x} =>
 (fun (a0 : A) (a' : D a0) (X0 : {x : _ & D x}) =>
  (fun (b0 : A) (b' : D b0) =>
   {f : a0 $<~> b0 & DCatEquiv f a' b'}) X0.1 X0.2)
   X.1 X.2) a b -> a $-> b
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall (a b : {x : _ & D x})
(f : (fun X : {x : _ & D x} =>
      (fun (a0 : A) (a' : D a0) (X0 : {x : _ & D x})
       =>
       (fun (b0 : A) (b' : D b0) =>
        {f : a0 $<~> b0 & DCatEquiv f a' b'}) X0.1
         X0.2) X.1 X.2) a b),
?CatIsEquiv' a b (?cate_fun' a b f)
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall (a b : {x : _ & D x}) 
(f : a $-> b),
?CatIsEquiv' a b f ->
(fun X : {x : _ & D x} =>
 (fun (a0 : A) (a' : D a0) (X0 : {x : _ & D x}) =>
  (fun (b0 : A) (b' : D b0) =>
   {f0 : a0 $<~> b0 & DCatEquiv f0 a' b'}) X0.1 X0.2)
   X.1 X.2) a b
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall (a b : {x : _ & D x}) 
(f : a $-> b) (fe : ?CatIsEquiv' a b f),
?cate_fun' a b (?cate_buildequiv' a b f fe) $== f
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall a b : {x : _ & D x},
(fun X : {x : _ & D x} =>
 (fun (a0 : A) (a' : D a0) (X0 : {x : _ & D x}) =>
  (fun (b0 : A) (b' : D b0) =>
   {f : a0 $<~> b0 & DCatEquiv f a' b'}) X0.1 X0.2)
   X.1 X.2) a b -> b $-> a
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall (a b : {x : _ & D x})
(f : (fun X : {x : _ & D x} =>
      (fun (a0 : A) (a' : D a0) (X0 : {x : _ & D x})
       =>
       (fun (b0 : A) (b' : D b0) =>
        {f : a0 $<~> b0 & DCatEquiv f a' b'}) X0.1
         X0.2) X.1 X.2) a b),
?cate_inv' a b f $o ?cate_fun' a b f $== Id a
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall (a b : {x : _ & D x})
(f : (fun X : {x : _ & D x} =>
      (fun (a0 : A) (a' : D a0) (X0 : {x : _ & D x})
       =>
       (fun (b0 : A) (b' : D b0) =>
        {f : a0 $<~> b0 & DCatEquiv f a' b'}) X0.1
         X0.2) X.1 X.2) a b),
?cate_fun' a b f $o ?cate_inv' a b f $== Id b
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
forall (a b : {x : _ & D x}) 
(f : a $-> b) (g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a -> ?CatIsEquiv' a b f
  all: intros aa' bb' [f f'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $-> bb'.1
f': DHom f aa'.2 bb'.2
Type
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $<~> bb'.1
f': DCatEquiv f aa'.2 bb'.2
aa' $-> bb'
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $<~> bb'.1
f': DCatEquiv f aa'.2 bb'.2
?Goal@{f:=?Goal0.1; f':=?Goal0.2}
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $-> bb'.1
f': DHom f aa'.2 bb'.2
?Goal ->
{f : aa'.1 $<~> bb'.1 & DCatEquiv f aa'.2 bb'.2}
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $-> bb'.1
f': DHom f aa'.2 bb'.2
forall fe : ?Goal,
?Goal0@{f:=(?Goal2 fe).1; f':=(?Goal2 fe).2} $==
(f; f')
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $<~> bb'.1
f': DCatEquiv f aa'.2 bb'.2
bb' $-> aa'
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $<~> bb'.1
f': DCatEquiv f aa'.2 bb'.2
?Goal4 $o ?Goal0 $== Id aa'
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $<~> bb'.1
f': DCatEquiv f aa'.2 bb'.2
?Goal0 $o ?Goal4 $== Id bb'
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $-> bb'.1
f': DHom f aa'.2 bb'.2
forall g : bb' $-> aa',
(f; f') $o g $== Id bb' ->
g $o (f; f') $== Id aa' -> ?Goal
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $-> bb'.1
f': DHom f aa'.2 bb'.2
Type exact {fe : CatIsEquiv f & DCatIsEquiv f'}.
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $<~> bb'.1
f': DCatEquiv f aa'.2 bb'.2
aa' $-> bb' exists f.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $<~> bb'.1
f': DCatEquiv f aa'.2 bb'.2
DHom f aa'.2 bb'.2 exact f'.
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $<~> bb'.1
f': DCatEquiv f aa'.2 bb'.2
{fe : CatIsEquiv (f; f').1 & DCatIsEquiv (f; f').2} exact (cate_isequiv f; dcate_isequiv f').
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $-> bb'.1
f': DHom f aa'.2 bb'.2
{fe : CatIsEquiv f & DCatIsEquiv f'} ->
{f : aa'.1 $<~> bb'.1 & DCatEquiv f aa'.2 bb'.2} intros [fe fe'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $-> bb'.1
f': DHom f aa'.2 bb'.2
fe: CatIsEquiv f
fe': DCatIsEquiv f'
{f : aa'.1 $<~> bb'.1 & DCatEquiv f aa'.2 bb'.2}
    exact (Build_CatEquiv f (fe:=fe); Build_DCatEquiv f' (fe':=fe')).
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $-> bb'.1
f': DHom f aa'.2 bb'.2
forall fe : {fe : CatIsEquiv f & DCatIsEquiv f'},
(((fun X : {fe0 : CatIsEquiv f & DCatIsEquiv f'} =>
   (fun (fe0 : CatIsEquiv f) (fe' : DCatIsEquiv f') =>
    (Build_CatEquiv f; Build_DCatEquiv f')) X.1 X.2)
    fe).1;
((fun X : {fe0 : CatIsEquiv f & DCatIsEquiv f'} =>
  (fun (fe0 : CatIsEquiv f) (fe' : DCatIsEquiv f') =>
   (Build_CatEquiv f; Build_DCatEquiv f')) X.1 X.2) fe).2) $==
(f; f') intros ?; exists (cate_buildequiv_fun f).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $-> bb'.1
f': DHom f aa'.2 bb'.2
fe: {fe : CatIsEquiv f & DCatIsEquiv f'}
DHom (cate_buildequiv_fun f) (Build_DCatEquiv f') f'
    exact (dcate_buildequiv_fun f').
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $<~> bb'.1
f': DCatEquiv f aa'.2 bb'.2
bb' $-> aa' exists (f^-1$).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $<~> bb'.1
f': DCatEquiv f aa'.2 bb'.2
DHom f^-1$ bb'.2 aa'.2 exact (f'^-1$').
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $<~> bb'.1
f': DCatEquiv f aa'.2 bb'.2
(f^-1$; f'^-1$') $o (f; f') $== Id aa' exact (cate_issect f; dcate_issect f').
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $<~> bb'.1
f': DCatEquiv f aa'.2 bb'.2
(f; f') $o (f^-1$; f'^-1$') $== Id bb' exact (cate_isretr f; dcate_isretr f').
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $-> bb'.1
f': DHom f aa'.2 bb'.2
forall g : bb' $-> aa',
(f; f') $o g $== Id bb' ->
g $o (f; f') $== Id aa' ->
{fe : CatIsEquiv f & DCatIsEquiv f'} intros [g g'] [r r'] [s s'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
aa', bb': {x : _ & D x}
f: aa'.1 $-> bb'.1
f': DHom f aa'.2 bb'.2
g: bb'.1 $-> aa'.1
g': DHom g bb'.2 aa'.2
r: ((f; f') $o (g; g')).1 $-> (Id bb').1
r': DHom r ((f; f') $o (g; g')).2 (Id bb').2
s: ((g; g') $o (f; f')).1 $-> (Id aa').1
s': DHom s ((g; g') $o (f; f')).2 (Id aa').2
{fe : CatIsEquiv f & DCatIsEquiv f'}
    exact (catie_adjointify f g r s; dcatie_adjointify f' g' r' s').
Defined.

(** The identity morphism is an equivalence *)
Instance dcatie_id {A} {D : A -> Type} `{DHasEquivs A D}
  {a : A} (a' : D a)
  : DCatIsEquiv (DId a')
  := dcatie_adjointify (DId a') (DId a') (dcat_idl (DId a')) (dcat_idr (DId a')).

Definition did_cate {A} {D : A -> Type} `{DHasEquivs A D}
  {a : A} (a' : D a)
  : DCatEquiv (id_cate a) a' a'
  := Build_DCatEquiv (DId a').

Instance reflexive_dcate {A} {D : A -> Type} `{DHasEquivs A D} {a : A}
  : Reflexive (DCatEquiv (id_cate a))
  := did_cate.

(** Anything homotopic to an equivalence is an equivalence. This should not be an instance. *)
Definition dcatie_homotopic {A} {D : A -> Type} `{DHasEquivs A D} {a b : A}
  {f : a $-> b} `{!CatIsEquiv f} {g : a $-> b} {p : f $== g} {a' : D a}
  {b' : D b} (f' : DHom f a' b') `{fe' : !DCatIsEquiv f'} {g' : DHom g a' b'}
  (p' : DGpdHom p f' g')
  : DCatIsEquiv (fe:=catie_homotopic f p) g'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
DCatIsEquiv g'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
DCatIsEquiv g'
  snapply dcatie_adjointify.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
DHom (Build_CatEquiv f)^-1$ b' a'
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
DGpdHom
  ((p^$ $@R (Build_CatEquiv f)^-1$) $@
   (((cate_buildequiv_fun f)^$ $@R
     (Build_CatEquiv f)^-1$) $@
    cate_isretr (Build_CatEquiv f))) 
  (g' $o' ?g') (DId b')
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
DGpdHom
  (((Build_CatEquiv f)^-1$ $@L p^$) $@
   (((Build_CatEquiv f)^-1$ $@L
     (cate_buildequiv_fun f)^$) $@
    cate_issect (Build_CatEquiv f))) 
  (?g' $o' g') (DId a')
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
DHom (Build_CatEquiv f)^-1$ b' a' exact (Build_DCatEquiv (fe':=fe') f')^-1$'.
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
DGpdHom
  ((p^$ $@R (Build_CatEquiv f)^-1$) $@
   (((cate_buildequiv_fun f)^$ $@R
     (Build_CatEquiv f)^-1$) $@
    cate_isretr (Build_CatEquiv f)))
  (g' $o' (Build_DCatEquiv f')^-1$') (DId b') refine (p'^$' $@R' _ $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
IsD0Gpd (fun f : a $-> b => DHom f a' b')
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
DGpdHom
  (((cate_buildequiv_fun f)^$ $@R
    (Build_CatEquiv f)^-1$) $@
   cate_isretr (Build_CatEquiv f))
  (f' $o' (Build_DCatEquiv f')^-1$') 
  (DId b')
    1: exact isd0gpd_hom.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
DGpdHom
  (((cate_buildequiv_fun f)^$ $@R
    (Build_CatEquiv f)^-1$) $@
   cate_isretr (Build_CatEquiv f))
  (f' $o' (Build_DCatEquiv f')^-1$') (DId b')
    refine ((dcate_buildequiv_fun f')^$' $@R' _ $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
IsD0Gpd (fun f : a $-> b => DHom f a' b')
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
DGpdHom (cate_isretr (Build_CatEquiv f))
  (dcate_buildequiv f' $o' (Build_DCatEquiv f')^-1$')
  (DId b')
    1: exact isd0gpd_hom.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
DGpdHom (cate_isretr (Build_CatEquiv f))
  (dcate_buildequiv f' $o' (Build_DCatEquiv f')^-1$')
  (DId b')
    apply dcate_isretr.
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
DGpdHom
  (((Build_CatEquiv f)^-1$ $@L p^$) $@
   (((Build_CatEquiv f)^-1$ $@L
     (cate_buildequiv_fun f)^$) $@
    cate_issect (Build_CatEquiv f)))
  ((Build_DCatEquiv f')^-1$' $o' g') (DId a') refine (_ $@L' p'^$' $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
IsD0Gpd (fun f : a $-> b => DHom f a' b')
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
DGpdHom
  (((Build_CatEquiv f)^-1$ $@L
    (cate_buildequiv_fun f)^$) $@
   cate_issect (Build_CatEquiv f))
  ((Build_DCatEquiv f')^-1$' $o' f') 
  (DId a')
    1: exact isd0gpd_hom.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
DGpdHom
  (((Build_CatEquiv f)^-1$ $@L
    (cate_buildequiv_fun f)^$) $@
   cate_issect (Build_CatEquiv f))
  ((Build_DCatEquiv f')^-1$' $o' f') (DId a')
    refine (_ $@L' (dcate_buildequiv_fun f')^$' $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
IsD0Gpd (fun f : a $-> b => DHom f a' b')
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
DGpdHom (cate_issect (Build_CatEquiv f))
  ((Build_DCatEquiv f')^-1$' $o' dcate_buildequiv f')
  (DId a')
    1: exact isd0gpd_hom.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
a': D a
b': D b
f': DHom f a' b'
fe': DCatIsEquiv f'
g': DHom g a' b'
p': DGpdHom p f' g'
DGpdHom (cate_issect (Build_CatEquiv f))
  ((Build_DCatEquiv f')^-1$' $o' dcate_buildequiv f')
  (DId a')
    apply dcate_issect.
Defined.

(** Equivalences can be composed. *)
Instance dcompose_catie {A} {D : A -> Type} `{DHasEquivs A D}
  {a b c : A} {g : b $<~> c} {f : a $<~> b} {a' : D a} {b' : D b} {c' : D c}
  (g' : DCatEquiv g b' c') (f' : DCatEquiv f a' b')
  : DCatIsEquiv (dcate_fun g' $o' f').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DCatIsEquiv (g' $o' f')
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DCatIsEquiv (g' $o' f')
  snapply dcatie_adjointify.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DHom (f^-1$ $o g^-1$) c' a'
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DGpdHom (compose_catie_isretr g f) 
  (g' $o' f' $o' ?g') (DId c')
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DGpdHom (compose_catie_issect g f)
  (?g' $o' (g' $o' f')) 
  (DId a')
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DHom (f^-1$ $o g^-1$) c' a' exact (dcate_fun f'^-1$' $o' g'^-1$').
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DGpdHom (compose_catie_isretr g f)
  (g' $o' f' $o' (f'^-1$' $o' g'^-1$')) (DId c') refine (dcat_assoc _ _ _ $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DGpdHom
  ((g $@L cat_assoc_opp g^-1$ f^-1$ f) $@
   ((g $@L (cate_isretr f $@R g^-1$)) $@
    ((g $@L cat_idl g^-1$) $@ cate_isretr g)))
  (g' $o' (f' $o' (f'^-1$' $o' g'^-1$'))) (DId c')
    refine (_ $@L' dcat_assoc_opp _ _ _ $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DGpdHom
  ((g $@L (cate_isretr f $@R g^-1$)) $@
   ((g $@L cat_idl g^-1$) $@ cate_isretr g))
  (g' $o' (f' $o' f'^-1$' $o' g'^-1$')) (DId c')
    refine (_ $@L' (dcate_isretr _ $@R' _) $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DGpdHom ((g $@L cat_idl g^-1$) $@ cate_isretr g)
  (g' $o' (DId b' $o' g'^-1$')) (DId c')
    refine (_ $@L' dcat_idl _ $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DGpdHom (cate_isretr g) (g' $o' g'^-1$') (DId c')
    apply dcate_isretr.
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DGpdHom (compose_catie_issect g f)
  (f'^-1$' $o' g'^-1$' $o' (g' $o' f')) (DId a') refine (dcat_assoc_opp _ _ _ $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DGpdHom
  ((f $@L cat_assoc_opp f^-1$ g^-1$ g) $@
   ((f $@L (cate_isretr g $@R f^-1$)) $@
    ((f $@L cat_idl f^-1$) $@ cate_isretr f)))
  (f'^-1$' $o' g'^-1$' $o' g' $o' f') (DId a')
    refine (dcat_assoc _ _ _ $@R' _ $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DGpdHom
  ((f $@L (cate_isretr g $@R f^-1$)) $@
   ((f $@L cat_idl f^-1$) $@ cate_isretr f))
  (f'^-1$' $o' (g'^-1$' $o' g') $o' f') (DId a')
    refine (((_ $@L' dcate_issect _) $@R' _) $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DGpdHom ((f $@L cat_idl f^-1$) $@ cate_isretr f)
  (f'^-1$' $o' DId b' $o' f') (DId a')
    refine ((dcat_idr _ $@R' _) $@' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DGpdHom (cate_isretr f) (f'^-1$' $o' f') (DId a')
    apply dcate_issect.
Defined.

Instance dcompose_catie' {A} {D : A -> Type} `{DHasEquivs A D}
  {a b c : A} {g : b $-> c} `{!CatIsEquiv g} {f : a $-> b} `{!CatIsEquiv f}
  {a' : D a} {b' : D b} {c' : D c}
  (g' : DHom g b' c') `{ge' : !DCatIsEquiv g'}
  (f' : DHom f a' b') `{fe' : !DCatIsEquiv f'}
  : DCatIsEquiv (fe:=compose_catie' g f) (g' $o' f').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $-> c
CatIsEquiv0: CatIsEquiv g
f: a $-> b
CatIsEquiv1: CatIsEquiv f
a': D a
b': D b
c': D c
g': DHom g b' c'
ge': DCatIsEquiv g'
f': DHom f a' b'
fe': DCatIsEquiv f'
DCatIsEquiv (g' $o' f')
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $-> c
CatIsEquiv0: CatIsEquiv g
f: a $-> b
CatIsEquiv1: CatIsEquiv f
a': D a
b': D b
c': D c
g': DHom g b' c'
ge': DCatIsEquiv g'
f': DHom f a' b'
fe': DCatIsEquiv f'
DCatIsEquiv (g' $o' f')
  pose (ff:=Build_DCatEquiv (fe':=fe') f').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $-> c
CatIsEquiv0: CatIsEquiv g
f: a $-> b
CatIsEquiv1: CatIsEquiv f
a': D a
b': D b
c': D c
g': DHom g b' c'
ge': DCatIsEquiv g'
f': DHom f a' b'
fe': DCatIsEquiv f'
ff:= Build_DCatEquiv f': DCatEquiv (Build_CatEquiv f) a' b'
DCatIsEquiv (g' $o' f')
  pose (gg:=Build_DCatEquiv (fe':=ge') g').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $-> c
CatIsEquiv0: CatIsEquiv g
f: a $-> b
CatIsEquiv1: CatIsEquiv f
a': D a
b': D b
c': D c
g': DHom g b' c'
ge': DCatIsEquiv g'
f': DHom f a' b'
fe': DCatIsEquiv f'
ff:= Build_DCatEquiv f': DCatEquiv (Build_CatEquiv f) a' b'
gg:= Build_DCatEquiv g': DCatEquiv (Build_CatEquiv g) b' c'
DCatIsEquiv (g' $o' f')
  nrefine (dcatie_homotopic (fe':=dcompose_catie gg ff) _ _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $-> c
CatIsEquiv0: CatIsEquiv g
f: a $-> b
CatIsEquiv1: CatIsEquiv f
a': D a
b': D b
c': D c
g': DHom g b' c'
ge': DCatIsEquiv g'
f': DHom f a' b'
fe': DCatIsEquiv f'
ff:= Build_DCatEquiv f': DCatEquiv (Build_CatEquiv f) a' b'
gg:= Build_DCatEquiv g': DCatEquiv (Build_CatEquiv g) b' c'
DGpdHom
  (cate_buildequiv_fun f $@@ cate_buildequiv_fun g)
  (gg $o' ff) (g' $o' f')
  exact (dcate_buildequiv_fun _ $@@' dcate_buildequiv_fun _).
Defined.

Definition dcompose_cate {A} {D : A -> Type} `{DHasEquivs A D}
  {a b c : A} {g : b $<~> c} {f : a $<~> b} {a' : D a} {b' : D b} {c' : D c}
  (g' : DCatEquiv g b' c') (f' : DCatEquiv f a' b')
  : DCatEquiv (compose_cate g f) a' c'
  := Build_DCatEquiv (dcate_fun g' $o' f').

Notation "g $oE' f" := (dcompose_cate g f).

(** Composing equivalences commutes with composing the underlying maps. *)
Definition dcompose_cate_fun {A} {D : A -> Type} `{DHasEquivs A D}
  {a b c : A} {g : b $<~> c} {f : a $<~> b} {a' : D a} {b' : D b} {c' : D c}
  (g' : DCatEquiv g b' c') (f' : DCatEquiv f a' b')
  : DGpdHom (compose_cate_fun g f)
    (dcate_fun (g' $oE' f')) (dcate_fun g' $o' f')
  := dcate_buildequiv_fun _.

Definition dcompose_cate_funinv {A} {D : A -> Type} `{DHasEquivs A D}
  {a b c : A} {g : b $<~> c} {f : a $<~> b} {a' : D a} {b' : D b} {c' : D c}
  (g' : DCatEquiv g b' c') (f' : DCatEquiv f a' b')
  : DGpdHom (compose_cate_funinv g f)
    (dcate_fun g' $o' f') (dcate_fun (g' $oE' f')).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DGpdHom (compose_cate_funinv g f) (g' $o' f')
  (g' $oE' f')
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DGpdHom (compose_cate_funinv g f) 
  (g' $o' f') (g' $oE' f')
  apply dgpd_rev.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
g: b $<~> c
f: a $<~> b
a': D a
b': D b
c': D c
g': DCatEquiv g b' c'
f': DCatEquiv f a' b'
DHom (cate_buildequiv_fun (g $o f)) 
  (g' $oE' f') (g' $o' f')
  apply dcate_buildequiv_fun.
Defined.

(** The underlying map of the identity equivalence is homotopic to the identity. *)
Definition did_cate_fun {A} {D : A -> Type} `{DHasEquivs A D} {a : A} (a' : D a)
  : DGpdHom (id_cate_fun a) (dcate_fun (did_cate a')) (DId a')
  := dcate_buildequiv_fun _.

(** Composition of equivalences is associative. *)
Definition dcompose_cate_assoc {A} {D : A -> Type} `{DHasEquivs A D}
  {a b c d : A} {f : a $<~> b} {g : b $<~> c} {h : c $<~> d} {a'} {b'} {c'} {d'}
  (f' : DCatEquiv f a' b') (g' : DCatEquiv g b' c') (h' : DCatEquiv h c' d')
  : DGpdHom (compose_cate_assoc f g h) (dcate_fun ((h' $oE' g') $oE' f'))
    (dcate_fun (h' $oE' (g' $oE' f'))).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c, d: A
f: a $<~> b
g: b $<~> c
h: c $<~> d
a': D a
b': D b
c': D c
d': D d
f': DCatEquiv f a' b'
g': DCatEquiv g b' c'
h': DCatEquiv h c' d'
DGpdHom (compose_cate_assoc f g h)
  (h' $oE' g' $oE' f') (h' $oE' (g' $oE' f'))
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c, d: A
f: a $<~> b
g: b $<~> c
h: c $<~> d
a': D a
b': D b
c': D c
d': D d
f': DCatEquiv f a' b'
g': DCatEquiv g b' c'
h': DCatEquiv h c' d'
DGpdHom (compose_cate_assoc f g h)
  (h' $oE' g' $oE' f') 
  (h' $oE' (g' $oE' f'))
  refine (dcompose_cate_fun _ f' $@' _ $@' dcat_assoc (dcate_fun f') g' h'
          $@' _ $@' dcompose_cate_funinv h' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c, d: A
f: a $<~> b
g: b $<~> c
h: c $<~> d
a': D a
b': D b
c': D c
d': D d
f': DCatEquiv f a' b'
g': DCatEquiv g b' c'
h': DCatEquiv h c' d'
DGpdHom (compose_cate_fun h g $@R f)
  (h' $oE' g' $o' f') (h' $o' g' $o' f')
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c, d: A
f: a $<~> b
g: b $<~> c
h: c $<~> d
a': D a
b': D b
c': D c
d': D d
f': DCatEquiv f a' b'
g': DCatEquiv g b' c'
h': DCatEquiv h c' d'
DGpdHom (h $@L compose_cate_funinv g f)
  (h' $o' (g' $o' f')) 
  (h' $o' (g' $oE' f'))
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c, d: A
f: a $<~> b
g: b $<~> c
h: c $<~> d
a': D a
b': D b
c': D c
d': D d
f': DCatEquiv f a' b'
g': DCatEquiv g b' c'
h': DCatEquiv h c' d'
DGpdHom (compose_cate_fun h g $@R f)
  (h' $oE' g' $o' f') (h' $o' g' $o' f') exact (dcompose_cate_fun h' g' $@R' _).
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c, d: A
f: a $<~> b
g: b $<~> c
h: c $<~> d
a': D a
b': D b
c': D c
d': D d
f': DCatEquiv f a' b'
g': DCatEquiv g b' c'
h': DCatEquiv h c' d'
DGpdHom (h $@L compose_cate_funinv g f)
  (h' $o' (g' $o' f')) 
  (h' $o' (g' $oE' f')) exact (_ $@L' dcompose_cate_funinv g' f').
Defined.

Definition dcompose_cate_idl {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {f : a $<~> b}  {a' : D a} {b' : D b} (f' : DCatEquiv f a' b')
  : DGpdHom (compose_cate_idl f) (dcate_fun (did_cate b' $oE' f'))
    (dcate_fun f').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DGpdHom (compose_cate_idl f) (did_cate b' $oE' f') f'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DGpdHom (compose_cate_idl f) (did_cate b' $oE' f') f'
  refine (dcompose_cate_fun _ f' $@' _ $@' dcat_idl (dcate_fun f')).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DGpdHom (cate_buildequiv_fun (Id b) $@R f)
  (did_cate b' $o' f') 
  (DId b' $o' f')
  exact (dcate_buildequiv_fun _ $@R' _).
Defined.

Definition dcompose_cate_idr {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {f : a $<~> b} {a' : D a} {b' : D b} (f' : DCatEquiv f a' b')
  : DGpdHom (compose_cate_idr f) (dcate_fun (f' $oE' did_cate a'))
    (dcate_fun f').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DGpdHom (compose_cate_idr f) (f' $oE' did_cate a') f'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DGpdHom (compose_cate_idr f) (f' $oE' did_cate a') f'
  refine (dcompose_cate_fun f' _ $@' _ $@' dcat_idr (dcate_fun f')).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
f: a $<~> b
a': D a
b': D b
f': DCatEquiv f a' b'
DGpdHom (cate_buildequiv_fun (Id a) $@R f)
  (f' $o' did_cate a') 
  (f' $o' DId a')
  exact (_ $@L' dcate_buildequiv_fun _).
Defined.

(** Some more convenient equalities for equivalences. The naming scheme is similar to [PathGroupoids.v].*)

Definition dcompose_V_hh {A} {D : A -> Type} `{DHasEquivs A D}
  {a b c : A} {f : b $<~> c} {g : a $-> b} {a' : D a} {b' : D b} {c' : D c}
  (f' : DCatEquiv f b' c') (g' : DHom g a' b')
  : DGpdHom (compose_V_hh f g) (dcate_fun f'^-1$' $o' (dcate_fun f' $o' g')) g'
  := (dcat_assoc_opp _ _ _) $@' (dcate_issect f' $@R' g') $@' dcat_idl g'.

Definition dcompose_h_Vh {A} {D : A -> Type} `{DHasEquivs A D}
  {a b c : A} {f : c $<~> b} {g : a $-> b} {a' : D a} {b' : D b} {c' : D c}
  (f' : DCatEquiv f c' b') (g' : DHom g a' b')
  : DGpdHom (compose_h_Vh f g) (dcate_fun f' $o' (dcate_fun f'^-1$' $o' g')) g'
  := (dcat_assoc_opp _ _ _) $@' (dcate_isretr f' $@R' g') $@' dcat_idl g'.

Definition dcompose_hh_V {A} {D : A -> Type} `{DHasEquivs A D}
  {a b c : A} {f : b $-> c} {g : a $<~> b} {a' : D a} {b' : D b} {c' : D c}
  (f' : DHom f b' c') (g' : DCatEquiv g a' b')
  : DGpdHom (compose_hh_V f g) ((f' $o' g') $o' g'^-1$') f'
  := dcat_assoc _ _ _ $@' (f' $@L' dcate_isretr g') $@' dcat_idr f'.

Definition dcompose_hV_h {A} {D : A -> Type} `{DHasEquivs A D}
  {a b c : A} {f : b $-> c} {g : b $<~> a} {a' : D a} {b' : D b} {c' : D c}
  (f' : DHom f b' c') (g' : DCatEquiv g b' a')
  : DGpdHom (compose_hV_h f g) ((f' $o' g'^-1$') $o' g') f'
  := dcat_assoc _ _ _ $@' (f' $@L' dcate_issect g') $@' dcat_idr f'.

(** Equivalences are both monomorphisms and epimorphisms (but not the converse). *)

Definition dcate_monic_equiv {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {e : a $<~> b} {a' : D a} {b' : D b} (e' : DCatEquiv e a' b')
  : DMonic (mon:=cate_monic_equiv e) (dcate_fun e').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
a': D a
b': D b
e': DCatEquiv e a' b'
DMonic e'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
a': D a
b': D b
e': DCatEquiv e a' b'
DMonic e'
  intros c f g p c' f' g' p'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
a': D a
b': D b
e': DCatEquiv e a' b'
c: A
f, g: c $-> a
p: e $o f $== e $o g
c': D c
f': DHom f c' a'
g': DHom g c' a'
p': DGpdHom p (e' $o' f') (e' $o' g')
DGpdHom (cate_monic_equiv e c f g p) f' g'
  refine ((dcompose_V_hh e' _)^$' $@' _ $@' dcompose_V_hh e' _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
a': D a
b': D b
e': DCatEquiv e a' b'
c: A
f, g: c $-> a
p: e $o f $== e $o g
c': D c
f': DHom f c' a'
g': DHom g c' a'
p': DGpdHom p (e' $o' f') (e' $o' g')
IsD0Gpd (fun f : c $-> a => DHom f c' a')
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
a': D a
b': D b
e': DCatEquiv e a' b'
c: A
f, g: c $-> a
p: e $o f $== e $o g
c': D c
f': DHom f c' a'
g': DHom g c' a'
p': DGpdHom p (e' $o' f') (e' $o' g')
DGpdHom (e^-1$ $@L p) (e'^-1$' $o' (e' $o' f'))
  (e'^-1$' $o' (e' $o' g'))
  1: exact isd0gpd_hom.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
a': D a
b': D b
e': DCatEquiv e a' b'
c: A
f, g: c $-> a
p: e $o f $== e $o g
c': D c
f': DHom f c' a'
g': DHom g c' a'
p': DGpdHom p (e' $o' f') (e' $o' g')
DGpdHom (e^-1$ $@L p) (e'^-1$' $o' (e' $o' f'))
  (e'^-1$' $o' (e' $o' g'))
  exact (_ $@L' p').
Defined.

Definition dcate_epic_equiv {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {e : a $<~> b} {a' : D a} {b' : D b} (e' : DCatEquiv e a' b')
  : DEpic (epi:=cate_epic_equiv e) (dcate_fun e').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
a': D a
b': D b
e': DCatEquiv e a' b'
DEpic e'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
a': D a
b': D b
e': DCatEquiv e a' b'
DEpic e'
  intros c f g p c' f' g' p'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
a': D a
b': D b
e': DCatEquiv e a' b'
c: A
f, g: b $-> c
p: f $o e $== g $o e
c': D c
f': DHom f b' c'
g': DHom g b' c'
p': DGpdHom p (f' $o' e') (g' $o' e')
DGpdHom (cate_epic_equiv e c f g p) f' g'
  refine ((dcompose_hh_V _ e')^$' $@' _ $@' dcompose_hh_V _ e').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
a': D a
b': D b
e': DCatEquiv e a' b'
c: A
f, g: b $-> c
p: f $o e $== g $o e
c': D c
f': DHom f b' c'
g': DHom g b' c'
p': DGpdHom p (f' $o' e') (g' $o' e')
IsD0Gpd (fun f : b $-> c => DHom f b' c')
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
a': D a
b': D b
e': DCatEquiv e a' b'
c: A
f, g: b $-> c
p: f $o e $== g $o e
c': D c
f': DHom f b' c'
g': DHom g b' c'
p': DGpdHom p (f' $o' e') (g' $o' e')
DGpdHom (e^-1$ $@L p) (f' $o' e' $o' e'^-1$')
  (g' $o' e' $o' e'^-1$')
  1: exact isd0gpd_hom.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
a': D a
b': D b
e': DCatEquiv e a' b'
c: A
f, g: b $-> c
p: f $o e $== g $o e
c': D c
f': DHom f b' c'
g': DHom g b' c'
p': DGpdHom p (f' $o' e') (g' $o' e')
DGpdHom (e^-1$ $@L p) (f' $o' e' $o' e'^-1$')
  (g' $o' e' $o' e'^-1$')
  exact (p' $@R' _).
Defined.

(** Some lemmas for moving equivalences around.  Naming based on EquivGroupoids.v. *)

Definition dcate_moveR_eM {A} {D : A -> Type} `{DHasEquivs A D}
  {a b c : A} {e : b $<~> a} {f : a $-> c} {g : b $-> c}
  {p : f $== g $o e^-1$} {a' : D a} {b' : D b} {c' : D c}
  (e' : DCatEquiv e b' a') (f' : DHom f a' c') (g' : DHom g b' c')
  (p' : DGpdHom p f' (g' $o' e'^-1$'))
  : DGpdHom (cate_moveR_eM e f g p) (f' $o' e') g'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
e: b $<~> a
f: a $-> c
g: b $-> c
p: f $== g $o e^-1$
a': D a
b': D b
c': D c
e': DCatEquiv e b' a'
f': DHom f a' c'
g': DHom g b' c'
p': DGpdHom p f' (g' $o' e'^-1$')
DGpdHom (cate_moveR_eM e f g p) (f' $o' e') g'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
e: b $<~> a
f: a $-> c
g: b $-> c
p: f $== g $o e^-1$
a': D a
b': D b
c': D c
e': DCatEquiv e b' a'
f': DHom f a' c'
g': DHom g b' c'
p': DGpdHom p f' (g' $o' e'^-1$')
DGpdHom (cate_moveR_eM e f g p) (f' $o' e') g'
  apply (dcate_epic_equiv e'^-1$').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
e: b $<~> a
f: a $-> c
g: b $-> c
p: f $== g $o e^-1$
a': D a
b': D b
c': D c
e': DCatEquiv e b' a'
f': DHom f a' c'
g': DHom g b' c'
p': DGpdHom p f' (g' $o' e'^-1$')
DGpdHom (compose_hh_V f e $@ p)
  (f' $o' e' $o' e'^-1$') 
  (g' $o' e'^-1$')
  exact (dcompose_hh_V _ _ $@' p').
Defined.

Definition dcate_moveR_Ve {A} {D : A -> Type} `{DHasEquivs A D}
  {a b c : A} {e : b $<~> c} {f : a $-> c} {g : a $-> b}
  {p : f $== e $o g} {a' : D a} {b' : D b} {c' : D c}
  (e' : DCatEquiv e b' c') (f' : DHom f a' c') (g' : DHom g a' b')
  (p' : DGpdHom p f' (dcate_fun e' $o' g'))
  : DGpdHom (cate_moveR_Ve e f g p) (dcate_fun e'^-1$' $o' f') g'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
e: b $<~> c
f: a $-> c
g: a $-> b
p: f $== e $o g
a': D a
b': D b
c': D c
e': DCatEquiv e b' c'
f': DHom f a' c'
g': DHom g a' b'
p': DGpdHom p f' (e' $o' g')
DGpdHom (cate_moveR_Ve e f g p) (e'^-1$' $o' f') g'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
e: b $<~> c
f: a $-> c
g: a $-> b
p: f $== e $o g
a': D a
b': D b
c': D c
e': DCatEquiv e b' c'
f': DHom f a' c'
g': DHom g a' b'
p': DGpdHom p f' (e' $o' g')
DGpdHom (cate_moveR_Ve e f g p) (e'^-1$' $o' f') g'
  apply (dcate_monic_equiv e').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
e: b $<~> c
f: a $-> c
g: a $-> b
p: f $== e $o g
a': D a
b': D b
c': D c
e': DCatEquiv e b' c'
f': DHom f a' c'
g': DHom g a' b'
p': DGpdHom p f' (e' $o' g')
DGpdHom (compose_hV_h f e $@ p)
  (e' $o' (e'^-1$' $o' f')) 
  (e' $o' g')
  exact (dcompose_h_Vh _ _ $@' p').
Defined.

Definition dcate_moveL_V1 {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {e : a $<~> b} {f : b $-> a} {p : e $o f $== Id b}
  {a' : D a} {b' : D b} {e' : DCatEquiv e a' b'}
  (f' : DHom f b' a') (p' : DGpdHom p (dcate_fun e' $o' f') (DId b'))
  : DGpdHom (cate_moveL_V1 f p) f' (dcate_fun e'^-1$').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
f: b $-> a
p: e $o f $== Id b
a': D a
b': D b
e': DCatEquiv e a' b'
f': DHom f b' a'
p': DGpdHom p (e' $o' f') (DId b')
DGpdHom (cate_moveL_V1 f p) f' e'^-1$'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
f: b $-> a
p: e $o f $== Id b
a': D a
b': D b
e': DCatEquiv e a' b'
f': DHom f b' a'
p': DGpdHom p (e' $o' f') (DId b')
DGpdHom (cate_moveL_V1 f p) f' e'^-1$'
  apply (dcate_monic_equiv e').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
f: b $-> a
p: e $o f $== Id b
a': D a
b': D b
e': DCatEquiv e a' b'
f': DHom f b' a'
p': DGpdHom p (e' $o' f') (DId b')
DGpdHom (p $@ (cate_isretr e)^$) 
  (e' $o' f') (e' $o' e'^-1$')
  napply (p' $@' (dcate_isretr e')^$').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
f: b $-> a
p: e $o f $== Id b
a': D a
b': D b
e': DCatEquiv e a' b'
f': DHom f b' a'
p': DGpdHom p (e' $o' f') (DId b')
IsD0Gpd (fun f : b $-> b => DHom f b' b')
  exact isd0gpd_hom.
Defined.

Definition dcate_moveL_1V {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {e : a $<~> b} {f : b $-> a} {p : f $o e $== Id a}
  {a' : D a} {b' : D b} {e' : DCatEquiv e a' b'}
  (f' : DHom f b' a') (p' : DGpdHom p (f' $o' e') (DId a'))
  : DGpdHom (cate_moveL_1V f p) f' (dcate_fun e'^-1$').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
f: b $-> a
p: f $o e $== Id a
a': D a
b': D b
e': DCatEquiv e a' b'
f': DHom f b' a'
p': DGpdHom p (f' $o' e') (DId a')
DGpdHom (cate_moveL_1V f p) f' e'^-1$'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
f: b $-> a
p: f $o e $== Id a
a': D a
b': D b
e': DCatEquiv e a' b'
f': DHom f b' a'
p': DGpdHom p (f' $o' e') (DId a')
DGpdHom (cate_moveL_1V f p) f' e'^-1$'
  apply (dcate_epic_equiv e').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
f: b $-> a
p: f $o e $== Id a
a': D a
b': D b
e': DCatEquiv e a' b'
f': DHom f b' a'
p': DGpdHom p (f' $o' e') (DId a')
DGpdHom (p $@ (cate_isretr e)^$) 
  (f' $o' e') (e'^-1$' $o' e')
  napply (p' $@' (dcate_issect e')^$').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
f: b $-> a
p: f $o e $== Id a
a': D a
b': D b
e': DCatEquiv e a' b'
f': DHom f b' a'
p': DGpdHom p (f' $o' e') (DId a')
IsD0Gpd (fun f : a $-> a => DHom f a' a')
  exact isd0gpd_hom.
Defined.

Definition dcate_moveR_V1 {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {e : a $<~> b} {f : b $-> a} {p : Id b $== e $o f}
  {a' : D a} {b' : D b} {e' : DCatEquiv e a' b'}
  (f' : DHom f b' a') (p' : DGpdHom p (DId b') (dcate_fun e' $o' f'))
  : DGpdHom (cate_moveR_V1 f p) (dcate_fun e'^-1$') f'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
f: b $-> a
p: Id b $== e $o f
a': D a
b': D b
e': DCatEquiv e a' b'
f': DHom f b' a'
p': DGpdHom p (DId b') (e' $o' f')
DGpdHom (cate_moveR_V1 f p) e'^-1$' f'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
f: b $-> a
p: Id b $== e $o f
a': D a
b': D b
e': DCatEquiv e a' b'
f': DHom f b' a'
p': DGpdHom p (DId b') (e' $o' f')
DGpdHom (cate_moveR_V1 f p) e'^-1$' f'
  apply (dcate_monic_equiv e').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
f: b $-> a
p: Id b $== e $o f
a': D a
b': D b
e': DCatEquiv e a' b'
f': DHom f b' a'
p': DGpdHom p (DId b') (e' $o' f')
DGpdHom (cate_isretr e $@ p) 
  (e' $o' e'^-1$') (e' $o' f')
  exact (dcate_isretr e' $@' p').
Defined.

Definition dcate_moveR_1V {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {e : a $<~> b} {f : b $-> a} {p : Id a $== f $o e}
  {a' : D a} {b' : D b} {e' : DCatEquiv e a' b'}
  (f' : DHom f b' a') (p' : DGpdHom p (DId a') (f' $o' e'))
  : DGpdHom (cate_moveR_1V f p) (dcate_fun e'^-1$') f'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
f: b $-> a
p: Id a $== f $o e
a': D a
b': D b
e': DCatEquiv e a' b'
f': DHom f b' a'
p': DGpdHom p (DId a') (f' $o' e')
DGpdHom (cate_moveR_1V f p) e'^-1$' f'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
f: b $-> a
p: Id a $== f $o e
a': D a
b': D b
e': DCatEquiv e a' b'
f': DHom f b' a'
p': DGpdHom p (DId a') (f' $o' e')
DGpdHom (cate_moveR_1V f p) e'^-1$' f'
  apply (dcate_epic_equiv e').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
f: b $-> a
p: Id a $== f $o e
a': D a
b': D b
e': DCatEquiv e a' b'
f': DHom f b' a'
p': DGpdHom p (DId a') (f' $o' e')
DGpdHom (cate_isretr e $@ p) 
  (e'^-1$' $o' e') (f' $o' e')
  exact (dcate_issect e' $@' p').
Defined.

(** Lemmas about the underlying map of an equivalence. *)

Definition dcate_inv2 {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {e f : a $<~> b} {p : cate_fun e $== cate_fun f}
  {a' : D a} {b' : D b} {e' : DCatEquiv e a' b'} {f' : DCatEquiv f a' b'}
  (p' : DGpdHom p (dcate_fun e') (dcate_fun f'))
  : DGpdHom (cate_inv2 p) (dcate_fun e'^-1$') (dcate_fun f'^-1$').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e, f: a $<~> b
p: e $== f
a': D a
b': D b
e': DCatEquiv e a' b'
f': DCatEquiv f a' b'
p': DGpdHom p e' f'
DGpdHom (cate_inv2 p) e'^-1$' f'^-1$'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e, f: a $<~> b
p: e $== f
a': D a
b': D b
e': DCatEquiv e a' b'
f': DCatEquiv f a' b'
p': DGpdHom p e' f'
DGpdHom (cate_inv2 p) e'^-1$' f'^-1$'
  apply dcate_moveL_V1.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e, f: a $<~> b
p: e $== f
a': D a
b': D b
e': DCatEquiv e a' b'
f': DCatEquiv f a' b'
p': DGpdHom p e' f'
DGpdHom ((p^$ $@R e^-1$) $@ cate_isretr e)
  (f' $o' e'^-1$') (DId b')
  rapply ((p'^$' $@R' _) $@' dcate_isretr _).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e, f: a $<~> b
p: e $== f
a': D a
b': D b
e': DCatEquiv e a' b'
f': DCatEquiv f a' b'
p': DGpdHom p e' f'
IsD0Gpd (fun f : a $-> b => DHom f a' b')
  exact isd0gpd_hom.
Defined.

Definition dcate_inv_compose {A} {D : A -> Type} `{DHasEquivs A D}
  {a b c : A} {e : a $<~> b} {f : b $<~> c} {a' : D a} {b' : D b} {c' : D c}
  (e' : DCatEquiv e a' b') (f' : DCatEquiv f b' c')
  : DGpdHom (cate_inv_compose e f)
    (dcate_fun (f' $oE' e')^-1$') (dcate_fun (e'^-1$' $oE' f'^-1$')).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
e: a $<~> b
f: b $<~> c
a': D a
b': D b
c': D c
e': DCatEquiv e a' b'
f': DCatEquiv f b' c'
DGpdHom (cate_inv_compose e f) (f' $oE' e')^-1$'
  (e'^-1$' $oE' f'^-1$')
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
e: a $<~> b
f: b $<~> c
a': D a
b': D b
c': D c
e': DCatEquiv e a' b'
f': DCatEquiv f b' c'
DGpdHom (cate_inv_compose e f) 
  (f' $oE' e')^-1$' (e'^-1$' $oE' f'^-1$')
  refine (_ $@' (dcompose_cate_fun e'^-1$' f'^-1$')^$').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
e: a $<~> b
f: b $<~> c
a': D a
b': D b
c': D c
e': DCatEquiv e a' b'
f': DCatEquiv f b' c'
DGpdHom
  (cate_inv_adjointify 
     (f $o e) (e^-1$ $o f^-1$)
     (compose_catie_isretr f e)
     (compose_catie_issect f e)) 
  (f' $oE' e')^-1$' (e'^-1$' $o' f'^-1$')
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
e: a $<~> b
f: b $<~> c
a': D a
b': D b
c': D c
e': DCatEquiv e a' b'
f': DCatEquiv f b' c'
IsD0Gpd (fun f : c $-> a => DHom f c' a')
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
e: a $<~> b
f: b $<~> c
a': D a
b': D b
c': D c
e': DCatEquiv e a' b'
f': DCatEquiv f b' c'
DGpdHom
  (cate_inv_adjointify 
     (f $o e) (e^-1$ $o f^-1$)
     (compose_catie_isretr f e)
     (compose_catie_issect f e)) 
  (f' $oE' e')^-1$' (e'^-1$' $o' f'^-1$') snapply dcate_inv_adjointify.
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b, c: A
e: a $<~> b
f: b $<~> c
a': D a
b': D b
c': D c
e': DCatEquiv e a' b'
f': DCatEquiv f b' c'
IsD0Gpd (fun f : c $-> a => DHom f c' a') exact isd0gpd_hom.
Defined.

Definition dcate_inv_V {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} {e : a $<~> b} {a' : D a} {b' : D b}
  (e' : DCatEquiv e a' b')
  : DGpdHom (cate_inv_V e) (dcate_fun (e'^-1$')^-1$') (dcate_fun e').A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
a': D a
b': D b
e': DCatEquiv e a' b'
DGpdHom (cate_inv_V e) (e'^-1$')^-1$' e'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
a': D a
b': D b
e': DCatEquiv e a' b'
DGpdHom (cate_inv_V e) (e'^-1$')^-1$' e'
  apply dcate_moveR_V1.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
a': D a
b': D b
e': DCatEquiv e a' b'
DGpdHom
  (symmetric_GpdHom (e^-1$ $o e) 
     (Id a) (cate_issect e)) 
  (DId a') (e'^-1$' $o' e')
  apply dgpd_rev.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
e: a $<~> b
a': D a
b': D b
e': DCatEquiv e a' b'
DHom (cate_issect e) (e'^-1$' $o' e') (DId a')
  apply dcate_issect.
Defined.

(** Any sufficiently coherent displayed functor preserves displayed equivalences. *)
Instance diemap {A B : Type}
  {DA : A -> Type} `{DHasEquivs A DA} {DB : B -> Type} `{DHasEquivs B DB}
  (F : A -> B) `{!Is0Functor F, !Is1Functor F}
  (F' : forall (a : A), DA a -> DB (F a)) `{!IsD0Functor F F', !IsD1Functor F F'}
  {a b : A} {f : a $<~> b} {a' : DA a} {b' : DA b} (f' : DCatEquiv f a' b')
  : DCatIsEquiv (fe:=iemap F f) (dfmap F F' (dcate_fun f')).A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
f: a $<~> b
a': DA a
b': DA b
f': DCatEquiv f a' b'
DCatIsEquiv (dfmap F F' f')
Proof.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
f: a $<~> b
a': DA a
b': DA b
f': DCatEquiv f a' b'
DCatIsEquiv (dfmap F F' f')
  refine (dcatie_adjointify
           (dfmap F F' (dcate_fun f')) (dfmap F F' (dcate_fun f'^-1$')) _ _).A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
f: a $<~> b
a': DA a
b': DA b
f': DCatEquiv f a' b'
DGpdHom
  (((fmap_comp F f^-1$ f)^$ $@ fmap2 F (cate_isretr f)) $@
   fmap_id F b) (dfmap F F' f' $o' dfmap F F' f'^-1$')
  (DId (F' b b'))
A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
f: a $<~> b
a': DA a
b': DA b
f': DCatEquiv f a' b'
DGpdHom
  (((fmap_comp F f f^-1$)^$ $@ fmap2 F (cate_issect f)) $@
   fmap_id F a) (dfmap F F' f'^-1$' $o' dfmap F F' f')
  (DId (F' a a'))
  -A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
f: a $<~> b
a': DA a
b': DA b
f': DCatEquiv f a' b'
DGpdHom
  (((fmap_comp F f^-1$ f)^$ $@ fmap2 F (cate_isretr f)) $@
   fmap_id F b) (dfmap F F' f' $o' dfmap F F' f'^-1$')
  (DId (F' b b')) refine ((dfmap_comp F F' (dcate_fun f'^-1$') f')^$' $@' _ $@' _).A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
f: a $<~> b
a': DA a
b': DA b
f': DCatEquiv f a' b'
DGpdHom (fmap2 F (cate_isretr f))
  (dfmap F F' (f' $o' f'^-1$')) 
  ?Goal0
A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
f: a $<~> b
a': DA a
b': DA b
f': DCatEquiv f a' b'
DGpdHom (fmap_id F b) ?Goal0 (DId (F' b b'))
    +A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
f: a $<~> b
a': DA a
b': DA b
f': DCatEquiv f a' b'
DGpdHom (fmap2 F (cate_isretr f))
  (dfmap F F' (f' $o' f'^-1$')) 
  ?Goal0 exact (dfmap2 F F' (dcate_isretr _)).
    +A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
f: a $<~> b
a': DA a
b': DA b
f': DCatEquiv f a' b'
DGpdHom (fmap_id F b) (dfmap F F' (DId b'))
  (DId (F' b b')) exact (dfmap_id F F' _).
  -A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
f: a $<~> b
a': DA a
b': DA b
f': DCatEquiv f a' b'
DGpdHom
  (((fmap_comp F f f^-1$)^$ $@ fmap2 F (cate_issect f)) $@
   fmap_id F a) (dfmap F F' f'^-1$' $o' dfmap F F' f')
  (DId (F' a a')) refine ((dfmap_comp F F' (dcate_fun f') f'^-1$')^$' $@' _ $@' _).A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
f: a $<~> b
a': DA a
b': DA b
f': DCatEquiv f a' b'
DGpdHom (fmap2 F (cate_issect f))
  (dfmap F F' (f'^-1$' $o' f')) 
  ?Goal
A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
f: a $<~> b
a': DA a
b': DA b
f': DCatEquiv f a' b'
DGpdHom (fmap_id F a) ?Goal (DId (F' a a'))
    +A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
f: a $<~> b
a': DA a
b': DA b
f': DCatEquiv f a' b'
DGpdHom (fmap2 F (cate_issect f))
  (dfmap F F' (f'^-1$' $o' f')) 
  ?Goal exact (dfmap2 F F' (dcate_issect _)).
    +A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
f: a $<~> b
a': DA a
b': DA b
f': DCatEquiv f a' b'
DGpdHom (fmap_id F a) (dfmap F F' (DId a'))
  (DId (F' a a')) exact (dfmap_id F F' _).
Defined.

Definition demap {A B : Type}
  {DA : A -> Type} `{DHasEquivs A DA} {DB : B -> Type} `{DHasEquivs B DB}
  (F : A -> B) `{!Is0Functor F, !Is1Functor F}
  (F' : forall (a : A), DA a -> DB (F a)) `{!IsD0Functor F F', !IsD1Functor F F'}
  {a b : A} {f : a $<~> b} {a' : DA a} {b' : DA b} (f' : DCatEquiv f a' b')
  : DCatEquiv (emap F f) (F' a a') (F' b b')
  := Build_DCatEquiv (dfmap F F' (dcate_fun f')).

Definition demap_id {A B : Type}
  {DA : A -> Type} `{DHasEquivs A DA} {DB : B -> Type} `{DHasEquivs B DB}
  (F : A -> B) `{!Is0Functor F, !Is1Functor F}
  (F' : forall (a : A), DA a -> DB (F a)) `{!IsD0Functor F F', !IsD1Functor F F'}
  {a : A} {a' : DA a}
  : DGpdHom (emap_id F)
    (dcate_fun (demap F F' (did_cate a'))) (dcate_fun (did_cate (F' a a'))).A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a: A
a': DA a
DGpdHom (emap_id F) (demap F F' (did_cate a'))
  (did_cate (F' a a'))
Proof.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a: A
a': DA a
DGpdHom (emap_id F) (demap F F' (did_cate a'))
  (did_cate (F' a a'))
  refine (dcate_buildequiv_fun _ $@' _).A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a: A
a': DA a
DGpdHom
  ((fmap2 F (id_cate_fun a) $@ fmap_id F a) $@
   (id_cate_fun (F a))^$) 
  (dfmap F F' (did_cate a')) 
  (did_cate (F' a a'))
  refine (dfmap2 F F' (did_cate_fun a') $@' _ $@' _).A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a: A
a': DA a
DGpdHom (fmap_id F a) (dfmap F F' (DId a')) ?Goal
A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a: A
a': DA a
DGpdHom (id_cate_fun (F a))^$ 
  ?Goal (did_cate (F' a a'))
  -A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a: A
a': DA a
DGpdHom (fmap_id F a) (dfmap F F' (DId a')) ?Goal rapply dfmap_id.
  -A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a: A
a': DA a
DGpdHom (id_cate_fun (F a))^$ 
  (DId (F' a a')) (did_cate (F' a a')) apply dgpd_rev.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a: A
a': DA a
DHom (id_cate_fun (F a)) 
  (did_cate (F' a a')) 
  (DId (F' a a'))
    exact (did_cate_fun (F' a a')).
Defined.

Definition demap_compose {A B : Type}
  {DA : A -> Type} `{DHasEquivs A DA} {DB : B -> Type} `{DHasEquivs B DB}
  (F : A -> B) `{!Is0Functor F, !Is1Functor F}
  (F' : forall (a : A), DA a -> DB (F a)) `{!IsD0Functor F F', isd1f : !IsD1Functor F F'}
  {a b c : A} {f : a $<~> b} {g : b $<~> c} {a' : DA a} {b' : DA b} {c' : DA c}
  (f' : DCatEquiv f a' b') (g' : DCatEquiv g b' c')
  : DGpdHom (emap_compose F f g) (dcate_fun (demap F F' (g' $oE' f')))
    (dfmap F F' (dcate_fun g') $o' dfmap F F' (dcate_fun f')).A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
isd1f: IsD1Functor F F'
a, b, c: A
f: a $<~> b
g: b $<~> c
a': DA a
b': DA b
c': DA c
f': DCatEquiv f a' b'
g': DCatEquiv g b' c'
DGpdHom (emap_compose F f g) (demap F F' (g' $oE' f'))
  (dfmap F F' g' $o' dfmap F F' f')
Proof.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
isd1f: IsD1Functor F F'
a, b, c: A
f: a $<~> b
g: b $<~> c
a': DA a
b': DA b
c': DA c
f': DCatEquiv f a' b'
g': DCatEquiv g b' c'
DGpdHom (emap_compose F f g) 
  (demap F F' (g' $oE' f'))
  (dfmap F F' g' $o' dfmap F F' f')
  refine (dcate_buildequiv_fun _ $@' _).A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
isd1f: IsD1Functor F F'
a, b, c: A
f: a $<~> b
g: b $<~> c
a': DA a
b': DA b
c': DA c
f': DCatEquiv f a' b'
g': DCatEquiv g b' c'
DGpdHom
  (fmap2 F (compose_cate_fun g f) $@ fmap_comp F f g)
  (dfmap F F' (g' $oE' f'))
  (dfmap F F' g' $o' dfmap F F' f')
  refine (dfmap2 F F' (dcompose_cate_fun _ _) $@' _).A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
isd1f: IsD1Functor F F'
a, b, c: A
f: a $<~> b
g: b $<~> c
a': DA a
b': DA b
c': DA c
f': DCatEquiv f a' b'
g': DCatEquiv g b' c'
DGpdHom (fmap_comp F f g) 
  (dfmap F F' (g' $o' f'))
  (dfmap F F' g' $o' dfmap F F' f')
  napply dfmap_comp; exact isd1f.
Defined.

(** A variant. *)
Definition demap_compose' {A B : Type}
  {DA : A -> Type} `{DHasEquivs A DA} {DB : B -> Type} `{DHasEquivs B DB}
  (F : A -> B) `{!Is0Functor F, !Is1Functor F}
  (F' : forall (a : A), DA a -> DB (F a)) `{!IsD0Functor F F', !IsD1Functor F F'}
  {a b c : A} {f : a $<~> b} {g : b $<~> c} {a' : DA a} {b' : DA b} {c' : DA c}
  (f' : DCatEquiv f a' b') (g' : DCatEquiv g b' c')
  : DGpdHom (emap_compose' F f g) (dcate_fun (demap F F' (g' $oE' f')))
    (dcate_fun ((demap F F' g') $oE' (demap F F' f'))).A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b, c: A
f: a $<~> b
g: b $<~> c
a': DA a
b': DA b
c': DA c
f': DCatEquiv f a' b'
g': DCatEquiv g b' c'
DGpdHom (emap_compose' F f g)
  (demap F F' (g' $oE' f'))
  (demap F F' g' $oE' demap F F' f')
Proof.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b, c: A
f: a $<~> b
g: b $<~> c
a': DA a
b': DA b
c': DA c
f': DCatEquiv f a' b'
g': DCatEquiv g b' c'
DGpdHom (emap_compose' F f g)
  (demap F F' (g' $oE' f'))
  (demap F F' g' $oE' demap F F' f')
  refine (demap_compose F F' f' g' $@' _).A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b, c: A
f: a $<~> b
g: b $<~> c
a': DA a
b': DA b
c': DA c
f': DCatEquiv f a' b'
g': DCatEquiv g b' c'
DGpdHom
  (symmetric_GpdHom (emap F g $oE emap F f)
     (fmap F g $o fmap F f)
     (compose_cate_fun (emap F g) (emap F f) $@
      (cate_buildequiv_fun (fmap F f) $@@
       cate_buildequiv_fun (fmap F g))))
  (dfmap F F' g' $o' dfmap F F' f')
  (demap F F' g' $oE' demap F F' f')
  apply dgpd_rev.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b, c: A
f: a $<~> b
g: b $<~> c
a': DA a
b': DA b
c': DA c
f': DCatEquiv f a' b'
g': DCatEquiv g b' c'
DHom
  (compose_cate_fun (emap F g) (emap F f) $@
   (cate_buildequiv_fun (fmap F f) $@@
    cate_buildequiv_fun (fmap F g)))
  (demap F F' g' $oE' demap F F' f')
  (dfmap F F' g' $o' dfmap F F' f')
  refine (dcompose_cate_fun _ _ $@' _).A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b, c: A
f: a $<~> b
g: b $<~> c
a': DA a
b': DA b
c': DA c
f': DCatEquiv f a' b'
g': DCatEquiv g b' c'
DGpdHom
  (cate_buildequiv_fun (fmap F f) $@@
   cate_buildequiv_fun (fmap F g))
  (demap F F' g' $o' demap F F' f')
  (dfmap F F' g' $o' dfmap F F' f')
  exact (dcate_buildequiv_fun _ $@@' dcate_buildequiv_fun _).
Defined.

Definition demap_inv {A B : Type}
  {DA : A -> Type} `{DHasEquivs A DA} {DB : B -> Type} `{DHasEquivs B DB}
  (F : A -> B) `{!Is0Functor F, !Is1Functor F}
  (F' : forall (a : A), DA a -> DB (F a)) `{!IsD0Functor F F', !IsD1Functor F F'}
  {a b : A} {e : a $<~> b} {a' : DA a} {b' : DA b} (e' : DCatEquiv e a' b')
  : DGpdHom (emap_inv F e)
    (dcate_fun (demap F F' e')^-1$') (dcate_fun (demap F F' e'^-1$')).A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
e: a $<~> b
a': DA a
b': DA b
e': DCatEquiv e a' b'
DGpdHom (emap_inv F e) (demap F F' e')^-1$'
  (demap F F' e'^-1$')
Proof.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
e: a $<~> b
a': DA a
b': DA b
e': DCatEquiv e a' b'
DGpdHom (emap_inv F e) 
  (demap F F' e')^-1$' 
  (demap F F' e'^-1$')
  refine (dcate_inv_adjointify _ _ _ _ $@' _).A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
e: a $<~> b
a': DA a
b': DA b
e': DCatEquiv e a' b'
DGpdHom (cate_buildequiv_fun (fmap F e^-1$))^$
  (dfmap F F' e'^-1$') 
  (demap F F' e'^-1$')
  apply dgpd_rev.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
IsD1Cat0: IsD1Cat DA
H1: DHasEquivs DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
IsD1Cat1: IsD1Cat DB
H4: DHasEquivs DB
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
a, b: A
e: a $<~> b
a': DA a
b': DA b
e': DCatEquiv e a' b'
DHom (cate_buildequiv_fun (fmap F e^-1$))
  (demap F F' e'^-1$') 
  (dfmap F F' e'^-1$')
  exact (dcate_buildequiv_fun _).
Defined.

(** When we have equivalences, we can define what it means for a displayed category to be univalent. *)
Definition dcat_equiv_path {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} (p : a = b) (a' : D a) (b' : D b)
  : transport D p a' = b' -> DCatEquiv (cat_equiv_path a b p) a' b'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
p: a = b
a': D a
b': D b
transport D p a' = b' ->
DCatEquiv (cat_equiv_path a b p) a' b'
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
p: a = b
a': D a
b': D b
transport D p a' = b' ->
DCatEquiv (cat_equiv_path a b p) a' b'
  intro p'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a, b: A
p: a = b
a': D a
b': D b
p': transport D p a' = b'
DCatEquiv (cat_equiv_path a b p) a' b' destruct p, p'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
H1: DHasEquivs D
a: A
a': D a
DCatEquiv (cat_equiv_path a a 1) a' (transport D 1 a') reflexivity.
Defined.

Class IsDUnivalent1Cat {A} (D : A -> Type) `{DHasEquivs A D} :=
{
  isequiv_dcat_equiv_path :: forall {a b : A} (p : a = b) a' b',
    IsEquiv (dcat_equiv_path p a' b')
}.

Definition dcat_path_equiv {A} {D : A -> Type} `{IsDUnivalent1Cat A D}
  {a b : A} (p : a = b) (a' : D a) (b' : D b)
  : DCatEquiv (cat_equiv_path a b p) a' b' -> transport D p a' = b'
  := (dcat_equiv_path p a' b')^-1.

(** If [IsUnivalent1Cat A] and [IsDUnivalent1Cat D], then this is an equivalence by [isequiv_functor_sigma]. *)
Definition dcat_equiv_path_total {A} {D : A -> Type} `{DHasEquivs A D}
  {a b : A} (a' : D a) (b' : D b)
  : {p : a = b & p # a' = b'} -> {e : a $<~> b & DCatEquiv e a' b'}
  := functor_sigma (cat_equiv_path a b) (fun p => dcat_equiv_path p a' b').

(** If the base category and the displayed category are both univalent, then the total category is univalent. *)
Instance isunivalent1cat_total {A} `{IsUnivalent1Cat A} (D : A -> Type)
  `{!IsDGraph D, !IsD2Graph D, !IsD01Cat D, !IsD1Cat D, !DHasEquivs D}
  `{!IsDUnivalent1Cat D}
  : IsUnivalent1Cat (sig D).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsUnivalent1Cat A
D: A -> Type
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
DHasEquivs0: DHasEquivs D
IsDUnivalent1Cat0: IsDUnivalent1Cat D
IsUnivalent1Cat {x : _ & D x}
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsUnivalent1Cat A
D: A -> Type
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
DHasEquivs0: DHasEquivs D
IsDUnivalent1Cat0: IsDUnivalent1Cat D
IsUnivalent1Cat {x : _ & D x}
  intros aa' bb'.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsUnivalent1Cat A
D: A -> Type
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
DHasEquivs0: DHasEquivs D
IsDUnivalent1Cat0: IsDUnivalent1Cat D
aa', bb': {x : _ & D x}
IsEquiv (cat_equiv_path aa' bb')
  apply (isequiv_homotopic
          (dcat_equiv_path_total _ _ o (path_sigma_uncurried D aa' bb')^-1)).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsUnivalent1Cat A
D: A -> Type
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
IsD1Cat0: IsD1Cat D
DHasEquivs0: DHasEquivs D
IsDUnivalent1Cat0: IsDUnivalent1Cat D
aa', bb': {x : _ & D x}
(fun x : aa' = bb' =>
 dcat_equiv_path_total aa'.2 bb'.2
   ((path_sigma_uncurried D aa' bb')^-1 x)) ==
cat_equiv_path aa' bb'
  intros []; reflexivity.
Defined.