Equiv.v

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

Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.Core.
Require Import WildCat.Opposite.

(** We declare a scope for printing [CatEquiv] as [≅] *)
Declare Scope wc_iso_scope.

(** * Equivalences in wild categories *)

(** We could define equivalences in any wild 1-category as bi-invertible maps, or in a wild 2-category as half-adjoint equivalences.  However, in concrete cases there is often an equivalent definition of equivalences that we want to use instead, and the important property we need is that it's logically equivalent to (quasi-)isomorphism. In [cat_hasequivs] below, we show that bi-invertible maps do provide a [HasEquivs] structure for any wild 1-category. *)

Class HasEquivs (A : Type) `{Is1Cat A} :=
{
  CatEquiv' : A -> A -> Type where "a $<~> b" := (CatEquiv' a b);
  CatIsEquiv' : forall a b, (a $-> b) -> Type;
  cate_fun' : forall a b, (a $<~> b) -> (a $-> b);
  cate_isequiv' : forall a b (f : a $<~> b), CatIsEquiv' a b (cate_fun' a b f);
  cate_buildequiv' : forall a b (f : a $-> b), CatIsEquiv' a b f -> CatEquiv' a b;
  cate_buildequiv_fun' : forall a b (f : a $-> b) (fe : CatIsEquiv' a b f),
      cate_fun' a b (cate_buildequiv' a b f fe) $== f;
  cate_inv' : forall a b (f : a $<~> b), b $-> a;
  cate_issect' : forall a b (f : a $<~> b),
    cate_inv' _ _ f $o cate_fun' _ _ f $== Id a;
  cate_isretr' : forall a b (f : a $<~> b),
      cate_fun' _ _ f $o cate_inv' _ _ f $== Id b;
  catie_adjointify' : forall a b (f : a $-> b) (g : b $-> a)
    (r : f $o g $== Id b) (s : g $o f $== Id a), CatIsEquiv' a b f;
}.

(** Since apparently a field of a record can't be the source of a coercion (Coq complains about the uniform inheritance condition, although as officially stated that condition appears to be satisfied), we redefine all the fields of [HasEquivs]. *)

Definition CatEquiv {A} `{HasEquivs A} (a b : A)
  := @CatEquiv' A _ _ _ _ _ a b.

Notation "a $<~> b" := (CatEquiv a b).
Infix "≅" := CatEquiv : wc_iso_scope.
Arguments CatEquiv : simpl never.

Definition cate_fun {A} `{HasEquivs A} {a b : A} (f : a $<~> b)
  : a $-> b
  := @cate_fun' A _ _ _ _ _ a b f.

Coercion cate_fun : CatEquiv >-> Hom.

(* Being an equivalence should be a typeclass, but we have to redefine it to work around https://github.com/coq/coq/issues/8994 . *)
Class CatIsEquiv {A} `{HasEquivs A} {a b : A} (f : a $-> b)
  := catisequiv : CatIsEquiv' a b f.

Global Instance cate_isequiv {A} `{HasEquivs A} {a b : A} (f : a $<~> b)
  : CatIsEquiv f
  := cate_isequiv' a b f.

Definition Build_CatEquiv {A} `{HasEquivs A} {a b : A}
           (f : a $-> b) {fe : CatIsEquiv f}
  : a $<~> b
  := cate_buildequiv' a b f fe.

Definition cate_buildequiv_fun {A} `{HasEquivs A} {a b : A}
           (f : a $-> b) {fe : CatIsEquiv f}
  : cate_fun (Build_CatEquiv f) $== f
  := cate_buildequiv_fun' a b f fe.

Definition catie_adjointify {A} `{HasEquivs A} {a b : A}
           (f : a $-> b) (g : b $-> a)
           (r : f $o g $== Id b) (s : g $o f $== Id a)
  : CatIsEquiv f
  := catie_adjointify' a b f g r s.

Definition cate_adjointify {A} `{HasEquivs A} {a b : A}
           (f : a $-> b) (g : b $-> a)
           (r : f $o g $== Id b) (s : g $o f $== Id a)
  : a $<~> b
  := Build_CatEquiv f (fe:=catie_adjointify f g r s).

(** This one we define to construct the whole inverse equivalence. *)
Definition cate_inv {A} `{HasEquivs A} {a b : A} (f : a $<~> b) : b $<~> a.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
b $<~> a
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
b $<~> a
  simple refine (cate_adjointify _ _ _ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
b $-> a
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
a $-> b
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
?f $o ?g $== Id a
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
?g $o ?f $== Id b
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
b $-> a exact (cate_inv' a b f).
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
a $-> b exact f.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
cate_inv' a b f $o f $== Id a exact (cate_issect' a b f).
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
f $o cate_inv' a b f $== Id b exact (cate_isretr' a b f).
Defined.

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

(** * Opposite categories preserve having equivalences. *)
Global Instance hasequivs_op {A} `{HasEquivs A} : HasEquivs A^op.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasEquivs A^op
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasEquivs A^op
  snrapply Build_HasEquivs; intros a b; unfold op in a, b; cbn.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
Type
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
(b $-> a) -> Type
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
?Goal -> b $-> a
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
forall f : ?Goal, ?Goal0 (?Goal1 f)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
forall f : b $-> a, ?Goal0 f -> ?Goal
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
forall (f : b $-> a) (fe : ?Goal0 f),
?Goal1 (?Goal3 f fe) $== f
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
?Goal -> a $-> b
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
forall f : ?Goal, ?Goal1 f $o ?Goal5 f $== Id a
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
forall f : ?Goal, ?Goal5 f $o ?Goal1 f $== Id b
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
forall (f : b $-> a) (g : a $-> b),
g $o f $== Id b -> f $o g $== Id a -> ?Goal0 f
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
Type exact (b $<~> a).
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
(b $-> a) -> Type apply CatIsEquiv.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
b $<~> a -> b $-> a apply cate_fun'.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
forall f : b $<~> a, CatIsEquiv (cate_fun' b a f) apply cate_isequiv'.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
forall f : b $-> a, CatIsEquiv f -> b $<~> a apply cate_buildequiv'.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
forall (f : b $-> a) (fe : CatIsEquiv f),
cate_fun' b a (cate_buildequiv' b a f fe) $== f rapply cate_buildequiv_fun'.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
b $<~> a -> a $-> b apply cate_inv'.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
forall f : b $<~> a,
cate_fun' b a f $o cate_inv' b a f $== Id a rapply cate_isretr'.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
forall f : b $<~> a,
cate_inv' b a f $o cate_fun' b a f $== Id b rapply cate_issect'.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
forall (f : b $-> a) (g : a $-> b),
g $o f $== Id b -> f $o g $== Id a -> CatIsEquiv f intros f g s t.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: b $-> a
g: a $-> b
s: g $o f $== Id b
t: f $o g $== Id a
CatIsEquiv f
    exact (catie_adjointify f g t s).
Defined.

Global Instance isequiv_op {A : Type} `{HasEquivs A}
       {a b : A} (f : a $-> b) {ief : CatIsEquiv f}
  : @CatIsEquiv A^op _ _ _ _ _ b a f
  := ief.

Definition cate_issect {A} `{HasEquivs A} {a b} (f : a $<~> b)
  : f^-1$ $o f $== Id a.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
f^-1$ $o f $== Id a
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
f^-1$ $o f $== Id a
  refine (_ $@ cate_issect' a b f).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
f^-1$ $o f $== cate_inv' a b f $o cate_fun' a b f
  refine (_ $@R f).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
f^-1$ $== cate_inv' a b f
  apply cate_buildequiv_fun'.
Defined.

Definition cate_isretr {A} `{HasEquivs A} {a b} (f : a $<~> b)
  : f $o f^-1$ $== Id b
  := cate_issect (A:=A^op) (b:=a) (a:=b) f.

(** If [g] is a section of an equivalence, then it is the inverse. *)
Definition cate_inverse_sect {A} `{HasEquivs A} {a b} (f : a $<~> b)
  (g : b $-> a) (p : f $o g $== Id b)
  : cate_fun f^-1$ $== g.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
g: b $-> a
p: f $o g $== Id b
f^-1$ $== g
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
g: b $-> a
p: f $o g $== Id b
f^-1$ $== g
  refine ((cat_idr _)^$ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
g: b $-> a
p: f $o g $== Id b
f^-1$ $o Id b $== g
  refine ((_ $@L p^$) $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
g: b $-> a
p: f $o g $== Id b
f^-1$ $o (f $o g) $== g
  refine (cat_assoc_opp _ _ _ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
g: b $-> a
p: f $o g $== Id b
f^-1$ $o f $o g $== g
  refine (cate_issect f $@R _ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
g: b $-> a
p: f $o g $== Id b
Id a $o g $== g
  apply cat_idl.
Defined.

(** If [g] is a retraction of an equivalence, then it is the inverse. *)
Definition cate_inverse_retr {A} `{HasEquivs A} {a b} (f : a $<~> b)
  (g : b $-> a) (p : g $o f $== Id a)
  : cate_fun f^-1$ $== g
  := cate_inverse_sect (A:=A^op) (a:=b) (b:=a) f g p.

(** It follows that the inverse of the equivalence you get by adjointification is homotopic to the inverse [g] provided. *)
Definition cate_inv_adjointify {A} `{HasEquivs A} {a b : A}
  (f : a $-> b) (g : b $-> a) (r : f $o g $== Id b) (s : g $o f $== Id a)
  : cate_fun (cate_adjointify f g r s)^-1$ $== g.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $-> b
g: b $-> a
r: f $o g $== Id b
s: g $o f $== Id a
(cate_adjointify f g r s)^-1$ $== g
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $-> b
g: b $-> a
r: f $o g $== Id b
s: g $o f $== Id a
(cate_adjointify f g r s)^-1$ $== g
  apply cate_inverse_sect.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $-> b
g: b $-> a
r: f $o g $== Id b
s: g $o f $== Id a
cate_adjointify f g r s $o g $== Id b
  exact ((cate_buildequiv_fun f $@R _) $@ r).
Defined.

(** The identity morphism is an equivalence *)
Global Instance catie_id {A} `{HasEquivs A} (a : A)
  : CatIsEquiv (Id a)
  := catie_adjointify (Id a) (Id a) (cat_idl (Id a)) (cat_idr (Id a)).

Definition id_cate {A} `{HasEquivs A} (a : A)
  : a $<~> a
  := Build_CatEquiv (Id a).

Global Instance reflexive_cate {A} `{HasEquivs A}
  : Reflexive (@CatEquiv A _ _ _ _ _)
  := id_cate.

Global Instance symmetric_cate {A} `{HasEquivs A}
  : Symmetric (@CatEquiv A _ _ _ _ _)
  := fun a b f => cate_inv f.

(** Anything homotopic to an equivalence is an equivalence. This should not be an instance. *)
Definition catie_homotopic {A} `{HasEquivs A} {a b : A}
  (f : a $-> b) `{!CatIsEquiv f} {g : a $-> b} (p : f $== g)
  : CatIsEquiv g.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
CatIsEquiv g
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
CatIsEquiv g
  snrapply catie_adjointify.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
b $-> a
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
g $o ?g $== Id b
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
?g $o g $== Id a
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
b $-> a exact (Build_CatEquiv f)^-1$.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
g $o (Build_CatEquiv f)^-1$ $== Id b refine (p^$ $@R _ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
f $o (Build_CatEquiv f)^-1$ $== Id b
    refine ((cate_buildequiv_fun f)^$ $@R _ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
Build_CatEquiv f $o (Build_CatEquiv f)^-1$ $== Id b
    apply cate_isretr.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
(Build_CatEquiv f)^-1$ $o g $== Id a refine (_ $@L p^$ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
(Build_CatEquiv f)^-1$ $o f $== Id a
    refine (_ $@L (cate_buildequiv_fun f)^$ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $-> b
CatIsEquiv0: CatIsEquiv f
g: a $-> b
p: f $== g
(Build_CatEquiv f)^-1$ $o Build_CatEquiv f $== Id a
    apply cate_issect.
Defined.

(** Equivalences can be composed.  In order to make use of duality, we factor out parts of the proof as two lemmas. *)

Definition compose_catie_isretr {A} `{HasEquivs A} {a b c : A}
  (g : b $<~> c) (f : a $<~> b)
  : g $o f $o (f^-1$ $o g^-1$) $== Id c.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
g: b $<~> c
f: a $<~> b
g $o f $o (f^-1$ $o g^-1$) $== Id c
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
g: b $<~> c
f: a $<~> b
g $o f $o (f^-1$ $o g^-1$) $== Id c
  refine (cat_assoc _ _ _ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
g: b $<~> c
f: a $<~> b
g $o (f $o (f^-1$ $o g^-1$)) $== Id c
  refine ((_ $@L cat_assoc_opp _ _ _) $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
g: b $<~> c
f: a $<~> b
g $o (f $o f^-1$ $o g^-1$) $== Id c
  refine ((_ $@L (cate_isretr _ $@R _)) $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
g: b $<~> c
f: a $<~> b
g $o (Id b $o g^-1$) $== Id c
  refine ((_ $@L cat_idl _) $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
g: b $<~> c
f: a $<~> b
g $o g^-1$ $== Id c
  apply cate_isretr.
Defined.

Definition compose_catie_issect {A} `{HasEquivs A} {a b c : A}
  (g : b $<~> c) (f : a $<~> b)
  : (f^-1$ $o g^-1$ $o (g $o f) $== Id a)
  := compose_catie_isretr (A:=A^op) (a:=c) (b:=b) (c:=a) f g.

Global Instance compose_catie {A} `{HasEquivs A} {a b c : A}
  (g : b $<~> c) (f : a $<~> b)
  : CatIsEquiv (g $o f).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
g: b $<~> c
f: a $<~> b
CatIsEquiv (g $o f)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
g: b $<~> c
f: a $<~> b
CatIsEquiv (g $o f)
  refine (catie_adjointify _ (f^-1$ $o g^-1$) _ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
g: b $<~> c
f: a $<~> b
g $o f $o (f^-1$ $o g^-1$) $== Id c
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
g: b $<~> c
f: a $<~> b
f^-1$ $o g^-1$ $o (g $o f) $== Id a
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
g: b $<~> c
f: a $<~> b
g $o f $o (f^-1$ $o g^-1$) $== Id c apply compose_catie_isretr.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
g: b $<~> c
f: a $<~> b
f^-1$ $o g^-1$ $o (g $o f) $== Id a apply compose_catie_issect.
Defined.

Global Instance compose_catie' {A} `{HasEquivs A} {a b c : A}
  (g : b $-> c) `{!CatIsEquiv g} (f : a $-> b) `{!CatIsEquiv f}
  : CatIsEquiv (g $o f)
  := catie_homotopic _ (cate_buildequiv_fun _ $@@ cate_buildequiv_fun _).

Definition compose_cate {A} `{HasEquivs A} {a b c : A}
  (g : b $<~> c) (f : a $<~> b) : a $<~> c
  := Build_CatEquiv (g $o f).

Notation "g $oE f" := (compose_cate g f).

Definition compose_cate_fun {A} `{HasEquivs A}
           {a b c : A} (g : b $<~> c) (f : a $<~> b)
  : cate_fun (g $oE f) $== g $o f.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
g: b $<~> c
f: a $<~> b
g $oE f $== g $o f
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
g: b $<~> c
f: a $<~> b
g $oE f $== g $o f
  apply cate_buildequiv_fun.
Defined.

Definition compose_cate_funinv {A} `{HasEquivs A}
           {a b c : A} (g : b $<~> c) (f : a $<~> b)
  : g $o f $== cate_fun (g $oE f).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
g: b $<~> c
f: a $<~> b
g $o f $== g $oE f
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
g: b $<~> c
f: a $<~> b
g $o f $== g $oE f
  apply gpd_rev.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
g: b $<~> c
f: a $<~> b
g $oE f $-> g $o f
  apply cate_buildequiv_fun.
Defined.

Definition id_cate_fun {A} `{HasEquivs A} (a : A)
  : cate_fun (id_cate a) $== Id a.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a: A
id_cate a $== Id a
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a: A
id_cate a $== Id a
  apply cate_buildequiv_fun.
Defined.

Definition compose_cate_assoc {A} `{HasEquivs A}
           {a b c d : A} (f : a $<~> b) (g : b $<~> c) (h : c $<~> d)
  : cate_fun ((h $oE g) $oE f) $== cate_fun (h $oE (g $oE f)).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c, d: A
f: a $<~> b
g: b $<~> c
h: c $<~> d
h $oE g $oE f $== h $oE (g $oE f)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c, d: A
f: a $<~> b
g: b $<~> c
h: c $<~> d
h $oE g $oE f $== h $oE (g $oE f)
  refine (compose_cate_fun _ f $@ _ $@ cat_assoc f g h $@ _ $@
                           compose_cate_funinv h _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c, d: A
f: a $<~> b
g: b $<~> c
h: c $<~> d
h $oE g $o f $== h $o g $o f
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c, d: A
f: a $<~> b
g: b $<~> c
h: c $<~> d
h $o (g $o f) $== h $o (g $oE f)
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c, d: A
f: a $<~> b
g: b $<~> c
h: c $<~> d
h $oE g $o f $== h $o g $o f refine (compose_cate_fun h g $@R _).
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c, d: A
f: a $<~> b
g: b $<~> c
h: c $<~> d
h $o (g $o f) $== h $o (g $oE f) refine (_ $@L compose_cate_funinv g f).
Defined.

Definition compose_cate_assoc_opp {A} `{HasEquivs A}
           {a b c d : A} (f : a $<~> b) (g : b $<~> c) (h : c $<~> d)
  : cate_fun (h $oE (g $oE f)) $== cate_fun ((h $oE g) $oE f).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c, d: A
f: a $<~> b
g: b $<~> c
h: c $<~> d
h $oE (g $oE f) $== h $oE g $oE f
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c, d: A
f: a $<~> b
g: b $<~> c
h: c $<~> d
h $oE (g $oE f) $== h $oE g $oE f
  Opaque compose_catie_isretr.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c, d: A
f: a $<~> b
g: b $<~> c
h: c $<~> d
h $oE (g $oE f) $== h $oE g $oE f
  (* We use [exact_no_check] just to save a small amount of time. *)
  exact_no_check (compose_cate_assoc (A:=A^op) (a:=d) (b:=c) (c:=b) (d:=a) h g f).
Defined.
Transparent compose_catie_isretr.

Definition compose_cate_idl {A} `{HasEquivs A}
           {a b : A} (f : a $<~> b)
  : cate_fun (id_cate b $oE f) $== cate_fun f.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
id_cate b $oE f $== f
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
id_cate b $oE f $== f
  refine (compose_cate_fun _ f $@ _ $@ cat_idl f).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: a $<~> b
id_cate b $o f $== Id b $o f
  refine (cate_buildequiv_fun _ $@R _).
Defined.

Definition compose_cate_idr {A} `{HasEquivs A}
           {a b : A} (f : a $<~> b)
  : cate_fun (f $oE id_cate a) $== cate_fun f
  := compose_cate_idl (A:=A^op) (a:=b) (b:=a) f.

Global Instance transitive_cate {A} `{HasEquivs A}
  : Transitive (@CatEquiv A _ _ _ _ _)
  := fun a b c f g => g $oE f.

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

Definition compose_V_hh {A} `{HasEquivs A} {a b c : A} (f : b $<~> c) (g : a $-> b) :
  f^-1$ $o (f $o g) $== g :=
  (cat_assoc_opp _ _ _) $@ (cate_issect f $@R g) $@ cat_idl g.

Definition compose_h_Vh {A} `{HasEquivs A} {a b c : A} (f : c $<~> b) (g : a $-> b) :
  f $o (f^-1$ $o g) $== g :=
  (cat_assoc_opp _ _ _) $@ (cate_isretr f $@R g) $@ cat_idl g.

Definition compose_hh_V {A} `{HasEquivs A} {a b c : A} (f : b $-> c) (g : a $<~> b) :
  (f $o g) $o g^-1$ $== f :=
  cat_assoc _ _ _ $@ (f $@L cate_isretr g) $@ cat_idr f.

Definition compose_hV_h {A} `{HasEquivs A} {a b c : A} (f : b $-> c) (g : b $<~> a) :
  (f $o g^-1$) $o g $== f :=
  cat_assoc _ _ _ $@ (f $@L cate_issect g) $@ cat_idr f.

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

Definition cate_monic_equiv {A} `{HasEquivs A} {a b : A} (e : a $<~> b)
  : Monic e.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: a $<~> b
Monic e
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: a $<~> b
Monic e
  intros c f g p.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: a $<~> b
c: A
f, g: c $-> a
p: e $o f $== e $o g
f $== g
  refine ((compose_V_hh e _)^$ $@ _ $@ compose_V_hh e _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: a $<~> b
c: A
f, g: c $-> a
p: e $o f $== e $o g
e^-1$ $o (e $o f) $== e^-1$ $o (e $o g)
  exact (_ $@L p).
Defined.

Definition cate_epic_equiv {A} `{HasEquivs A} {a b : A} (e : a $<~> b)
  : Epic e
  := cate_monic_equiv (A:=A^op) (a:=b) (b:=a) e.

(** ** Movement Lemmas *)

(** These lemmas can be used to move equivalences around in an equation. *)

Definition cate_moveL_eM {A} `{HasEquivs A} {a b c : A}
  (e : a $<~> b) (f : a $-> c) (g : b $-> c)
  (p : f $o e^-1$ $== g)
  : f $== g $o e.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
e: a $<~> b
f: a $-> c
g: b $-> c
p: f $o e^-1$ $== g
f $== g $o e
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
e: a $<~> b
f: a $-> c
g: b $-> c
p: f $o e^-1$ $== g
f $== g $o e
  apply (cate_epic_equiv e^-1$).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
e: a $<~> b
f: a $-> c
g: b $-> c
p: f $o e^-1$ $== g
f $o e^-1$ $== g $o e $o e^-1$
  exact (p $@ (compose_hh_V _ _)^$).
Defined.

Definition cate_moveR_eM {A} `{HasEquivs A} {a b c : A}
  (e : b $<~> a) (f : a $-> c) (g : b $-> c)
  (p : f $== g $o e^-1$)
  : f $o e $== g.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
e: b $<~> a
f: a $-> c
g: b $-> c
p: f $== g $o e^-1$
f $o e $== g
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
e: b $<~> a
f: a $-> c
g: b $-> c
p: f $== g $o e^-1$
f $o e $== g
  apply (cate_epic_equiv e^-1$).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
e: b $<~> a
f: a $-> c
g: b $-> c
p: f $== g $o e^-1$
f $o e $o e^-1$ $== g $o e^-1$
  exact (compose_hh_V _ _ $@ p).
Defined.

Definition cate_moveL_Me {A} `{HasEquivs A} {a b c : A}
  (e : b $<~> c) (f : a $-> c) (g : a $-> b)
  (p : e^-1$ $o f $== g)
  : f $== e $o g
  := cate_moveL_eM (A:=A^op) (a:=c) (b:=b) (c:=a) e f g p.

Definition cate_moveR_Me {A} `{HasEquivs A} {a b c : A}
  (e : c $<~> b) (f : a $-> c) (g : a $-> b)
  (p : f $== e^-1$ $o g)
  : e $o f $== g
  := cate_moveR_eM (A:=A^op) (a:=c) (b:=b) (c:=a) e f g p.

Definition cate_moveL_eV {A} `{HasEquivs A} {a b c : A}
  (e : a $<~> b) (f : b $-> c) (g : a $-> c)
  (p : f $o e $== g)
  : f $== g $o e^-1$.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
e: a $<~> b
f: b $-> c
g: a $-> c
p: f $o e $== g
f $== g $o e^-1$
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
e: a $<~> b
f: b $-> c
g: a $-> c
p: f $o e $== g
f $== g $o e^-1$
  apply (cate_epic_equiv e).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
e: a $<~> b
f: b $-> c
g: a $-> c
p: f $o e $== g
f $o e $== g $o e^-1$ $o e
  exact (p $@ (compose_hV_h _ _)^$).
Defined.

Definition cate_moveR_eV {A} `{HasEquivs A} {a b c : A}
  (e : b $<~> a) (f : b $-> c) (g : a $-> c)
  (p : f $== g $o e)
  : f $o e^-1$ $== g.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
e: b $<~> a
f: b $-> c
g: a $-> c
p: f $== g $o e
f $o e^-1$ $== g
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
e: b $<~> a
f: b $-> c
g: a $-> c
p: f $== g $o e
f $o e^-1$ $== g
  apply (cate_epic_equiv e).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
e: b $<~> a
f: b $-> c
g: a $-> c
p: f $== g $o e
f $o e^-1$ $o e $== g $o e
  exact (compose_hV_h _ _ $@ p).
Defined.

Definition cate_moveL_Ve {A} `{HasEquivs A} {a b c : A}
  (e : b $<~> c) (f : a $-> b) (g : a $-> c)
  (p : e $o f $== g)
  : f $== e^-1$ $o g
  := cate_moveL_eV (A:=A^op) (a:=c) (b:=b) (c:=a) e f g p.

Definition cate_moveR_Ve {A} `{HasEquivs A} {a b c : A}
  (e : b $<~> c) (f : a $-> c) (g : a $-> b)
  (p : f $== e $o g)
  : e^-1$ $o f $== g
  := cate_moveR_eV (A:=A^op) (a:=b) (b:=c) (c:=a) e f g p.

Definition cate_moveL_V1 {A} `{HasEquivs A} {a b : A} {e : a $<~> b} (f : b $-> a)
  (p : e $o f $== Id _)
  : f $== cate_fun e^-1$.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: a $<~> b
f: b $-> a
p: e $o f $== Id b
f $== e^-1$
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: a $<~> b
f: b $-> a
p: e $o f $== Id b
f $== e^-1$
  apply (cate_monic_equiv e).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: a $<~> b
f: b $-> a
p: e $o f $== Id b
e $o f $== e $o e^-1$
  exact (p $@ (cate_isretr e)^$).
Defined.

Definition cate_moveL_1V {A} `{HasEquivs A} {a b : A} {e : a $<~> b} (f : b $-> a)
  (p : f $o e $== Id _)
  : f $== cate_fun e^-1$
  := cate_moveL_V1 (A:=A^op) (a:=b) (b:=a) f p.

Definition cate_moveR_V1 {A} `{HasEquivs A} {a b : A} {e : a $<~> b} (f : b $-> a)
  (p : Id _ $== e $o f)
  : cate_fun e^-1$ $== f.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: a $<~> b
f: b $-> a
p: Id b $== e $o f
e^-1$ $== f
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: a $<~> b
f: b $-> a
p: Id b $== e $o f
e^-1$ $== f
  apply (cate_monic_equiv e).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: a $<~> b
f: b $-> a
p: Id b $== e $o f
e $o e^-1$ $== e $o f
  exact (cate_isretr e $@ p).
Defined.

Definition cate_moveR_1V {A} `{HasEquivs A} {a b : A} {e : a $<~> b} (f : b $-> a)
  (p : Id _ $== f $o e)
  : cate_fun e^-1$ $== f
  := cate_moveR_V1 (A:=A^op) (a:=b) (b:=a) f p.

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

Definition cate_inv2 {A} `{HasEquivs A} {a b : A} {e f : a $<~> b} (p : cate_fun e $== cate_fun f)
  : cate_fun e^-1$ $== cate_fun f^-1$.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e, f: a $<~> b
p: e $== f
e^-1$ $== f^-1$
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e, f: a $<~> b
p: e $== f
e^-1$ $== f^-1$
  apply cate_moveL_V1.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e, f: a $<~> b
p: e $== f
f $o e^-1$ $== Id b
  exact ((p^$ $@R _) $@ cate_isretr _).
Defined.

Definition cate_inv_compose {A} `{HasEquivs A} {a b c : A} (e : a $<~> b) (f : b $<~> c)
  : cate_fun (f $oE e)^-1$ $== cate_fun (e^-1$ $oE f^-1$).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
e: a $<~> b
f: b $<~> c
(f $oE e)^-1$ $== e^-1$ $oE f^-1$
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
e: a $<~> b
f: b $<~> c
(f $oE e)^-1$ $== e^-1$ $oE f^-1$
  refine (_ $@ (compose_cate_fun _ _)^$).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: A
e: a $<~> b
f: b $<~> c
(f $oE e)^-1$ $== e^-1$ $o f^-1$
  apply cate_inv_adjointify.
Defined.

Definition cate_inv_V {A} `{HasEquivs A} {a b : A} (e : a $<~> b)
  : cate_fun (e^-1$)^-1$ $== cate_fun e.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: a $<~> b
(e^-1$)^-1$ $== e
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: a $<~> b
(e^-1$)^-1$ $== e
  apply cate_moveR_V1.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: a $<~> b
Id a $== e^-1$ $o e
  symmetry; apply cate_issect.
Defined.

(** Any sufficiently coherent functor preserves equivalences.  *)
Global Instance iemap {A B : Type} `{HasEquivs A} `{HasEquivs B}
       (F : A -> B) `{!Is0Functor F, !Is1Functor F}
       {a b : A} (f : a $<~> b)
  : CatIsEquiv (fmap F f).A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b: A
f: a $<~> b
CatIsEquiv (fmap F f)
Proof.A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b: A
f: a $<~> b
CatIsEquiv (fmap F f)
  refine (catie_adjointify (fmap F f) (fmap F f^-1$) _ _).A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b: A
f: a $<~> b
fmap F f $o fmap F f^-1$ $== Id (F b)
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b: A
f: a $<~> b
fmap F f^-1$ $o fmap F f $== Id (F a)
  -A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b: A
f: a $<~> b
fmap F f $o fmap F f^-1$ $== Id (F b) refine ((fmap_comp F f^-1$ f)^$ $@ fmap2 F (cate_isretr _) $@ fmap_id F _).
  -A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b: A
f: a $<~> b
fmap F f^-1$ $o fmap F f $== Id (F a) refine ((fmap_comp F f f^-1$)^$ $@ fmap2 F (cate_issect _) $@ fmap_id F _).
Defined.

Definition emap {A B : Type} `{HasEquivs A} `{HasEquivs B}
           (F : A -> B) `{!Is0Functor F, !Is1Functor F}
           {a b : A} (f : a $<~> b)
  : F a $<~> F b
  := Build_CatEquiv (fmap F f).

Definition emap_id {A B : Type} `{HasEquivs A} `{HasEquivs B}
  (F : A -> B) `{!Is0Functor F, !Is1Functor F} {a : A}
  : cate_fun (emap F (id_cate a)) $== cate_fun (id_cate (F a)).A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a: A
emap F (id_cate a) $== id_cate (F a)
Proof.A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a: A
emap F (id_cate a) $== id_cate (F a)
  refine (cate_buildequiv_fun _ $@ _).A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a: A
fmap F (id_cate a) $== id_cate (F a)
  refine (fmap2 F (id_cate_fun a) $@ _ $@ (id_cate_fun (F a))^$).A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a: A
fmap F (Id a) $== Id (F a)
  rapply fmap_id.
Defined.

Definition emap_compose {A B : Type} `{HasEquivs A} `{HasEquivs B}
  (F : A -> B) `{!Is0Functor F, !Is1Functor F}
  {a b c : A} (f : a $<~> b) (g : b $<~> c)
  : cate_fun (emap F (g $oE f)) $== fmap F (cate_fun g) $o fmap F (cate_fun f).A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b, c: A
f: a $<~> b
g: b $<~> c
emap F (g $oE f) $== fmap F g $o fmap F f
Proof.A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b, c: A
f: a $<~> b
g: b $<~> c
emap F (g $oE f) $== fmap F g $o fmap F f
  refine (cate_buildequiv_fun _ $@ _).A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b, c: A
f: a $<~> b
g: b $<~> c
fmap F (g $oE f) $== fmap F g $o fmap F f
  refine (fmap2 F (compose_cate_fun _ _) $@ _).A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b, c: A
f: a $<~> b
g: b $<~> c
fmap F (g $o f) $== fmap F g $o fmap F f
  rapply fmap_comp.
Defined.

(** A variant. *)
Definition emap_compose' {A B : Type} `{HasEquivs A} `{HasEquivs B}
  (F : A -> B) `{!Is0Functor F, !Is1Functor F}
  {a b c : A} (f : a $<~> b) (g : b $<~> c)
  : cate_fun (emap F (g $oE f)) $== cate_fun ((emap F g) $oE (emap F f)).A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b, c: A
f: a $<~> b
g: b $<~> c
emap F (g $oE f) $== emap F g $oE emap F f
Proof.A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b, c: A
f: a $<~> b
g: b $<~> c
emap F (g $oE f) $== emap F g $oE emap F f
  refine (emap_compose F f g $@ _).A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b, c: A
f: a $<~> b
g: b $<~> c
fmap F g $o fmap F f $== emap F g $oE emap F f
  symmetry.A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b, c: A
f: a $<~> b
g: b $<~> c
emap F g $oE emap F f $== fmap F g $o fmap F f
  refine (compose_cate_fun _ _ $@ _).A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b, c: A
f: a $<~> b
g: b $<~> c
emap F g $o emap F f $== fmap F g $o fmap F f
  exact (cate_buildequiv_fun _ $@@ cate_buildequiv_fun _).
Defined.

Definition emap_inv {A B : Type} `{HasEquivs A} `{HasEquivs B}
  (F : A -> B) `{!Is0Functor F, !Is1Functor F}
  {a b : A} (e : a $<~> b)
  : cate_fun (emap F e)^-1$ $== cate_fun (emap F e^-1$).A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b: A
e: a $<~> b
(emap F e)^-1$ $== emap F e^-1$
Proof.A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b: A
e: a $<~> b
(emap F e)^-1$ $== emap F e^-1$
  refine (cate_inv_adjointify _ _ _ _ $@ _).A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
a, b: A
e: a $<~> b
fmap F e^-1$ $== emap F e^-1$
  exact (cate_buildequiv_fun _)^$.
Defined.

(** When we have equivalences, we can define what it means for a category to be univalent. *)
Definition cat_equiv_path {A : Type} `{HasEquivs A} (a b : A)
  : (a = b) -> (a $<~> b).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
a = b -> a $<~> b
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
a = b -> a $<~> b
  intros []; reflexivity.
Defined.

Class IsUnivalent1Cat (A : Type) `{HasEquivs A}
  := { isequiv_cat_equiv_path : forall a b, IsEquiv (@cat_equiv_path A _ _ _ _ _ a b) }.
Global Existing Instance isequiv_cat_equiv_path.

Definition cat_path_equiv {A : Type} `{IsUnivalent1Cat A} (a b : A)
  : (a $<~> b) -> (a = b)
  := (cat_equiv_path a b)^-1.

(** ** Core of a 1-category *)

Record core (A : Type) := { uncore : A }.
Arguments uncore {A} c.
Arguments Build_core {A} a : rename.

Global Instance isgraph_core {A : Type} `{HasEquivs A}
  : IsGraph (core A).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph (core A)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph (core A)
  srapply Build_IsGraph.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
core A -> core A -> Type
  intros a b ; exact (uncore a $<~> uncore b).
Defined.

Global Instance is01cat_core {A : Type} `{HasEquivs A}
  : Is01Cat (core A).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is01Cat (core A)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is01Cat (core A)
  srapply Build_Is01Cat ; cbv.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall a : core A, CatEquiv' (uncore a) (uncore a)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall a b c : core A,
CatEquiv' (uncore b) (uncore c) ->
CatEquiv' (uncore a) (uncore b) ->
CatEquiv' (uncore a) (uncore c)
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall a : core A, CatEquiv' (uncore a) (uncore a) intros; apply id_cate.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall a b c : core A,
CatEquiv' (uncore b) (uncore c) ->
CatEquiv' (uncore a) (uncore b) ->
CatEquiv' (uncore a) (uncore c) intros a b c ; apply compose_cate.
Defined.

Global Instance is2graph_core {A : Type} `{HasEquivs A}
  : Is2Graph (core A).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is2Graph (core A)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is2Graph (core A)
  intros a b.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
IsGraph (a $-> b)
  apply Build_IsGraph.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
(a $-> b) -> (a $-> b) -> Type
  intros f g ; exact (cate_fun f $== cate_fun g).
Defined.

Global Instance is01cat_core_hom {A : Type} `{HasEquivs A} (a b : core A)
  : Is01Cat (a $-> b).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
Is01Cat (a $-> b)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
Is01Cat (a $-> b)
  srapply Build_Is01Cat.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
forall a0 : a $-> b, a0 $-> a0
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
forall a0 b0 c : a $-> b,
(b0 $-> c) -> (a0 $-> b0) -> a0 $-> c
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
forall a0 : a $-> b, a0 $-> a0 intro f; cbn; apply Id.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
forall a0 b0 c : a $-> b,
(b0 $-> c) -> (a0 $-> b0) -> a0 $-> c intros f g h; cbn; apply cat_comp.
Defined.

Global Instance is0gpd_core_hom {A : Type} `{HasEquivs A} (a b : core A)
  : Is0Gpd (a $-> b).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
Is0Gpd (a $-> b)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
Is0Gpd (a $-> b)
  apply Build_Is0Gpd.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
forall a0 b0 : a $-> b, (a0 $-> b0) -> b0 $-> a0
  intros f g ; cbv.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f, g: a $-> b
(cate_fun' (uncore a) (uncore b) f $->
 cate_fun' (uncore a) (uncore b) g) ->
cate_fun' (uncore a) (uncore b) g $->
cate_fun' (uncore a) (uncore b) f
  apply gpd_rev.
Defined.

Global Instance is0functor_core_postcomp {A : Type} `{HasEquivs A}
       (a b c : core A) (h : b $-> c) :
  Is0Functor (cat_postcomp a h).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: core A
h: b $-> c
Is0Functor (cat_postcomp a h)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: core A
h: b $-> c
Is0Functor (cat_postcomp a h)
  apply Build_Is0Functor.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: core A
h: b $-> c
forall a0 b0 : a $-> b,
(a0 $-> b0) ->
cat_postcomp a h a0 $-> cat_postcomp a h b0
  intros f g al; cbn in h.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: core A
h: uncore b $<~> uncore c
f, g: a $-> b
al: f $-> g
cat_postcomp a h f $-> cat_postcomp a h g
  exact (compose_cate_fun h f
           $@ (h $@L al)
           $@ (compose_cate_fun h g)^$).
Defined.

Global Instance is0functor_core_precomp {A : Type} `{HasEquivs A}
       (a b c : core A) (h : a $-> b) :
  Is0Functor (cat_precomp c h).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: core A
h: a $-> b
Is0Functor (cat_precomp c h)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: core A
h: a $-> b
Is0Functor (cat_precomp c h)
  apply Build_Is0Functor.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: core A
h: a $-> b
forall a0 b0 : b $-> c,
(a0 $-> b0) ->
cat_precomp c h a0 $-> cat_precomp c h b0
  intros f g al; cbn in h.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: core A
h: uncore a $<~> uncore b
f, g: b $-> c
al: f $-> g
cat_precomp c h f $-> cat_precomp c h g
  (** Why can't coq resolve this? *)
  refine (compose_cate_fun f h
           $@ (_ $@R h)
           $@ (compose_cate_fun g h)^$).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b, c: core A
h: uncore a $<~> uncore b
f, g: b $-> c
al: f $-> g
f $== g
  exact al.
Defined.

Global Instance is1cat_core {A : Type} `{HasEquivs A}
  : Is1Cat (core A).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is1Cat (core A)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is1Cat (core A)
  rapply Build_Is1Cat.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b c d : core A) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o g $o f $== h $o (g $o f)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b c d : core A) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o (g $o f) $== h $o g $o f
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b : core A) (f : a $-> b), Id b $o f $== f
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b : core A) (f : a $-> b), f $o Id a $== f
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b c d : core A) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o g $o f $== h $o (g $o f) intros; apply compose_cate_assoc.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b c d : core A) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o (g $o f) $== h $o g $o f intros; apply compose_cate_assoc_opp.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b : core A) (f : a $-> b), Id b $o f $== f intros; apply compose_cate_idl.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b : core A) (f : a $-> b), f $o Id a $== f intros; apply compose_cate_idr.
Defined.

Global Instance is0gpd_core {A : Type} `{HasEquivs A}
  : Is0Gpd (core A).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Gpd (core A)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Gpd (core A)
  apply Build_Is0Gpd.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall a b : core A, (a $-> b) -> b $-> a
  intros a b f; cbn in *; exact (f^-1$).
Defined.

Global Instance is1gpd_core {A : Type} `{HasEquivs A}
  : Is1Gpd (core A).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is1Gpd (core A)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is1Gpd (core A)
  apply Build_Is1Gpd; cbn ; intros a b f;
    refine (compose_cate_fun _ _ $@ _ $@ (id_cate_fun _)^$).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: uncore a $<~> uncore b
f^-1$ $o f $== Id (uncore a)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: uncore a $<~> uncore b
f $o f^-1$ $== Id (uncore b)
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: uncore a $<~> uncore b
f^-1$ $o f $== Id (uncore a) apply cate_issect.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: uncore a $<~> uncore b
f $o f^-1$ $== Id (uncore b) apply cate_isretr.
Defined.

Global Instance hasequivs_core {A : Type} `{HasEquivs A}
  : HasEquivs (core A).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasEquivs (core A)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasEquivs (core A)
  srapply Build_HasEquivs.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
core A -> core A -> Type
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall a b : core A, (a $-> b) -> Type
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall a b : core A, ?CatEquiv' a b -> a $-> b
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b : core A) (f : ?CatEquiv' a b),
?CatIsEquiv' a b (?cate_fun' a b f)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b : core A) (f : a $-> b),
?CatIsEquiv' a b f -> ?CatEquiv' a b
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b : core A) (f : a $-> b)
(fe : ?CatIsEquiv' a b f),
?cate_fun' a b (?cate_buildequiv' a b f fe) $== f
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall a b : core A, ?CatEquiv' a b -> b $-> a
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b : core A) (f : ?CatEquiv' a b),
?cate_inv' a b f $o ?cate_fun' a b f $== Id a
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b : core A) (f : ?CatEquiv' a b),
?cate_fun' a b f $o ?cate_inv' a b f $== Id b
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b : core A) (f : a $-> b) 
(g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a -> ?CatIsEquiv' a b f
  1: exact (fun a b => a $-> b).  (* In [core A], i.e. [CatEquiv' (uncore a) (uncore b)]. *)A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall a b : core A, (a $-> b) -> Type
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall a b : core A,
(fun a0 b0 : core A => a0 $-> b0) a b -> a $-> b
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b : core A)
(f : (fun a0 b0 : core A => a0 $-> b0) a b),
?CatIsEquiv' a b (?cate_fun' a b f)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b : core A) (f : a $-> b),
?CatIsEquiv' a b f ->
(fun a0 b0 : core A => a0 $-> b0) a b
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b : core A) (f : a $-> b)
(fe : ?CatIsEquiv' a b f),
?cate_fun' a b (?cate_buildequiv' a b f fe) $== f
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall a b : core A,
(fun a0 b0 : core A => a0 $-> b0) a b -> b $-> a
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b : core A)
(f : (fun a0 b0 : core A => a0 $-> b0) a b),
?cate_inv' a b f $o ?cate_fun' a b f $== Id a
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b : core A)
(f : (fun a0 b0 : core A => a0 $-> b0) a b),
?cate_fun' a b f $o ?cate_inv' a b f $== Id b
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
forall (a b : core A) (f : a $-> b) 
(g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a -> ?CatIsEquiv' a b f
  all: intros a b f; cbn; intros.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: a $-> b
Type
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: (fun a b : core A => a $-> b) a b
uncore a $<~> uncore b
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: (fun a b : core A => a $-> b) a b
?Goal@{f:=?Goal0}
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: a $-> b
X: ?Goal
uncore a $<~> uncore b
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: a $-> b
fe: ?Goal
?Goal0@{f:=(fun H1 : ?Goal => ?Goal5@{X:=H1}) fe} $==
f
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: (fun a b : core A => a $-> b) a b
uncore b $<~> uncore a
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: (fun a b : core A => a $-> b) a b
?Goal2 $oE ?Goal0 $== id_cate (uncore a)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: (fun a b : core A => a $-> b) a b
?Goal0 $oE ?Goal2 $== id_cate (uncore b)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: a $-> b
g: uncore b $<~> uncore a
r: f $oE g $== id_cate (uncore b)
s: g $oE f $== id_cate (uncore a)
?Goal
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: a $-> b
Type exact Unit.  (* Or [CatIsEquiv' (uncore a) (uncore b) (cate_fun f)]? *)
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: (fun a b : core A => a $-> b) a b
uncore a $<~> uncore b exact f.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: (fun a b : core A => a $-> b) a b
Unit exact tt.    (* Or [cate_isequiv' _ _ _]? *)
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: a $-> b
X: Unit
uncore a $<~> uncore b exact f.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: a $-> b
fe: Unit
(fun _ : Unit => f) fe $== f reflexivity.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: (fun a b : core A => a $-> b) a b
uncore b $<~> uncore a exact f^-1$.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: (fun a b : core A => a $-> b) a b
f^-1$ $oE f $== id_cate (uncore a) refine (compose_cate_fun _ _ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: (fun a b : core A => a $-> b) a b
f^-1$ $o f $== id_cate (uncore a)
    refine (cate_issect _ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: (fun a b : core A => a $-> b) a b
Id (uncore a) $== id_cate (uncore a)
    symmetry; apply id_cate_fun.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: (fun a b : core A => a $-> b) a b
f $oE f^-1$ $== id_cate (uncore b) refine (compose_cate_fun _ _ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: (fun a b : core A => a $-> b) a b
f $o f^-1$ $== id_cate (uncore b)
    refine (cate_isretr _ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: (fun a b : core A => a $-> b) a b
Id (uncore b) $== id_cate (uncore b)
    symmetry; apply id_cate_fun.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: core A
f: a $-> b
g: uncore b $<~> uncore a
r: f $oE g $== id_cate (uncore b)
s: g $oE f $== id_cate (uncore a)
Unit exact tt.
Defined.

Global Instance hasmorext_core {A : Type} `{HasEquivs A, !HasMorExt A}
  `{forall x y (f g : uncore x $<~> uncore y), IsEquiv (ap (x := f) (y := g) cate_fun)} 
  : HasMorExt (core A).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
H1: forall (x y : core A)
(f g : uncore x $<~> uncore y),
IsEquiv (ap cate_fun)
HasMorExt (core A)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
H1: forall (x y : core A)
(f g : uncore x $<~> uncore y),
IsEquiv (ap cate_fun)
HasMorExt (core A)
  snrapply Build_HasMorExt.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
H1: forall (x y : core A)
(f g : uncore x $<~> uncore y),
IsEquiv (ap cate_fun)
forall (a b : core A) (f g : a $-> b),
IsEquiv GpdHom_path
  intros X Y f g; cbn in *.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
H1: forall (x y : core A)
(f g : uncore x $<~> uncore y),
IsEquiv (ap cate_fun)
X, Y: core A
f, g: uncore X $<~> uncore Y
IsEquiv GpdHom_path
  snrapply isequiv_homotopic.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
H1: forall (x y : core A)
(f g : uncore x $<~> uncore y),
IsEquiv (ap cate_fun)
X, Y: core A
f, g: uncore X $<~> uncore Y
f = g -> f $== g
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
H1: forall (x y : core A)
(f g : uncore x $<~> uncore y),
IsEquiv (ap cate_fun)
X, Y: core A
f, g: uncore X $<~> uncore Y
IsEquiv ?f
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
H1: forall (x y : core A)
(f g : uncore x $<~> uncore y),
IsEquiv (ap cate_fun)
X, Y: core A
f, g: uncore X $<~> uncore Y
?f == GpdHom_path
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
H1: forall (x y : core A)
(f g : uncore x $<~> uncore y),
IsEquiv (ap cate_fun)
X, Y: core A
f, g: uncore X $<~> uncore Y
f = g -> f $== g exact (GpdHom_path o (ap (x:=f) (y:=g) cate_fun)).
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
H1: forall (x y : core A)
(f g : uncore x $<~> uncore y),
IsEquiv (ap cate_fun)
X, Y: core A
f, g: uncore X $<~> uncore Y
IsEquiv (GpdHom_path o ap cate_fun) rapply isequiv_compose.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
H1: forall (x y : core A)
(f g : uncore x $<~> uncore y),
IsEquiv (ap cate_fun)
X, Y: core A
f, g: uncore X $<~> uncore Y
GpdHom_path o ap cate_fun == GpdHom_path intro p; by induction p.
Defined.

(** * Initial objects and terminal objects are all respectively equivalent. *)

Lemma cate_isinitial A `{HasEquivs A} (x y : A)
  : IsInitial x -> IsInitial y -> x $<~> y.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
x, y: A
IsInitial x -> IsInitial y -> x $<~> y
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
x, y: A
IsInitial x -> IsInitial y -> x $<~> y
  intros inx iny.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
x, y: A
inx: IsInitial x
iny: IsInitial y
x $<~> y
  srapply (cate_adjointify (inx y).1 (iny x).1).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
x, y: A
inx: IsInitial x
iny: IsInitial y
(inx y).1 $o (iny x).1 $== Id y
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
x, y: A
inx: IsInitial x
iny: IsInitial y
(iny x).1 $o (inx y).1 $== Id x
  1: exact (((iny _).2 _)^$ $@ (iny _).2 _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
x, y: A
inx: IsInitial x
iny: IsInitial y
(iny x).1 $o (inx y).1 $== Id x
  1: exact (((inx _).2 _)^$ $@ (inx _).2 _).
Defined.

Definition cate_isterminal A `{HasEquivs A} (x y : A)
  : IsTerminal x -> IsTerminal y -> y $<~> x
  := cate_isinitial A^op x y.

Lemma isinitial_cate A `{HasEquivs A} (x y : A)
  : x $<~> y -> IsInitial x -> IsInitial y.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
x, y: A
x $<~> y -> IsInitial x -> IsInitial y
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
x, y: A
x $<~> y -> IsInitial x -> IsInitial y
  intros f inx z.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
x, y: A
f: x $<~> y
inx: IsInitial x
z: A
{f : y $-> z & forall g : y $-> z, f $== g}
  exists ((inx z).1 $o f^-1$).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
x, y: A
f: x $<~> y
inx: IsInitial x
z: A
forall g : y $-> z, (inx z).1 $o f^-1$ $== g
  intros g.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
x, y: A
f: x $<~> y
inx: IsInitial x
z: A
g: y $-> z
(inx z).1 $o f^-1$ $== g
  refine (_ $@ compose_hh_V _ f).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
x, y: A
f: x $<~> y
inx: IsInitial x
z: A
g: y $-> z
(inx z).1 $o f^-1$ $== g $o f $o f^-1$
  refine (_ $@R _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
x, y: A
f: x $<~> y
inx: IsInitial x
z: A
g: y $-> z
(inx z).1 $== g $o f
  exact ((inx z).2 _).
Defined.

Definition isterminal_cate A `{HasEquivs A} (x y : A)
  : y $<~> x -> IsTerminal x -> IsTerminal y
  := isinitial_cate A^op x y.

(** * There is a default notion of equivalence for a 1-category, namely bi-invertibility. *)

(** We do not use the half-adjoint definition, since we can't prove adjointification for that definition. *)

Class Cat_IsBiInv {A} `{Is1Cat A} {x y : A} (f : x $-> y) := {
  cat_equiv_inv : y $-> x;
  cat_eisretr : f $o cat_equiv_inv $== Id y;
  cat_equiv_inv' : y $-> x;
  cat_eissect' : cat_equiv_inv' $o f $== Id x;
}.

Arguments cat_equiv_inv {A}%type_scope { _ _ _ _ x y} f {_}.
Arguments cat_eisretr {A}%type_scope { _ _ _ _ x y} f {_}.
Arguments cat_equiv_inv' {A}%type_scope { _ _ _ _ x y} f {_}.
Arguments cat_eissect' {A}%type_scope { _ _ _ _ x y} f {_}.

Arguments Build_Cat_IsBiInv {A}%type_scope {_ _ _ _ x y f} cat_equiv_inv cat_eisretr cat_equiv_inv' cat_eissect'.

Record Cat_BiInv A `{Is1Cat A} (x y : A) := {
  cat_equiv_fun :> x $-> y;
  cat_equiv_isequiv : Cat_IsBiInv cat_equiv_fun;
}.

Global Existing Instance cat_equiv_isequiv.

(** The two inverses are necessarily homotopic. *)
Definition cat_inverses_homotopic {A} `{Is1Cat A} {x y : A} (f : x $-> y) {bif : Cat_IsBiInv f}
  : cat_equiv_inv f $== cat_equiv_inv' f.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: x $-> y
bif: Cat_IsBiInv f
cat_equiv_inv f $== cat_equiv_inv' f
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: x $-> y
bif: Cat_IsBiInv f
cat_equiv_inv f $== cat_equiv_inv' f
  refine ((cat_idl _)^$ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: x $-> y
bif: Cat_IsBiInv f
Id x $o cat_equiv_inv f $== cat_equiv_inv' f
  refine (cat_prewhisker (cat_eissect' f)^$ _ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: x $-> y
bif: Cat_IsBiInv f
cat_equiv_inv' f $o f $o cat_equiv_inv f $==
cat_equiv_inv' f
  refine (cat_assoc _ _ _ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: x $-> y
bif: Cat_IsBiInv f
cat_equiv_inv' f $o (f $o cat_equiv_inv f) $==
cat_equiv_inv' f
  refine (cat_postwhisker _ (cat_eisretr f) $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: x $-> y
bif: Cat_IsBiInv f
cat_equiv_inv' f $o Id y $== cat_equiv_inv' f
  apply cat_idr.
Defined.

(** Therefore we can prove [eissect] for the first inverse as well. *)
Definition cat_eissect {A} `{Is1Cat A} {x y : A} (f : x $-> y) {bif : Cat_IsBiInv f}
  : cat_equiv_inv f $o f $== Id x
  := (cat_inverses_homotopic f $@R f) $@ cat_eissect' f.

(** This shows that any 1-category satisfies [HasEquivs].  We do not make it an instance, since we may want to use a different [HasEquivs] structure in particular cases. *)
Definition cat_hasequivs A `{Is1Cat A} : HasEquivs A.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasEquivs A
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasEquivs A
  srapply Build_HasEquivs; intros x y.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
Type
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
(x $-> y) -> Type
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
(fun x y : A => ?Goal) x y -> x $-> y
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
forall f : (fun x y : A => ?Goal) x y,
(fun x y : A => ?Goal0) x y
  ((fun x y : A => ?Goal1) x y f)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
forall f : x $-> y,
(fun x y : A => ?Goal0) x y f ->
(fun x y : A => ?Goal) x y
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
forall (f : x $-> y)
(fe : (fun x y : A => ?Goal0) x y f),
(fun x y : A => ?Goal1) x y
  ((fun x y : A => ?Goal3) x y f fe) $== f
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
(fun x y : A => ?Goal) x y -> y $-> x
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
forall f : (fun x y : A => ?Goal) x y,
(fun x y : A => ?Goal5) x y f $o
(fun x y : A => ?Goal1) x y f $== 
Id x
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
forall f : (fun x y : A => ?Goal) x y,
(fun x y : A => ?Goal1) x y f $o
(fun x y : A => ?Goal5) x y f $== 
Id y
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
forall (f : x $-> y) (g : y $-> x),
f $o g $== Id y ->
g $o f $== Id x -> (fun x y : A => ?Goal0) x y f
  1: exact (Cat_BiInv _ x y).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
(x $-> y) -> Type
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
(fun x y : A => Cat_BiInv A x y) x y -> x $-> y
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
forall f : (fun x y : A => Cat_BiInv A x y) x y,
(fun x y : A => ?Goal) x y
  ((fun x y : A => ?Goal0) x y f)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
forall f : x $-> y,
(fun x y : A => ?Goal) x y f ->
(fun x y : A => Cat_BiInv A x y) x y
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
forall (f : x $-> y)
(fe : (fun x y : A => ?Goal) x y f),
(fun x y : A => ?Goal0) x y
  ((fun x y : A => ?Goal2) x y f fe) $== f
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
(fun x y : A => Cat_BiInv A x y) x y -> y $-> x
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
forall f : (fun x y : A => Cat_BiInv A x y) x y,
(fun x y : A => ?Goal4) x y f $o
(fun x y : A => ?Goal0) x y f $== 
Id x
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
forall f : (fun x y : A => Cat_BiInv A x y) x y,
(fun x y : A => ?Goal0) x y f $o
(fun x y : A => ?Goal4) x y f $== 
Id y
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
forall (f : x $-> y) (g : y $-> x),
f $o g $== Id y ->
g $o f $== Id x -> (fun x y : A => ?Goal) x y f
  all:intros f; cbn beta in *.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: x $-> y
Type
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: Cat_BiInv A x y
x $-> y
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: Cat_BiInv A x y
?Goal@{f:=?Goal0}
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: x $-> y
?Goal -> Cat_BiInv A x y
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: x $-> y
forall fe : ?Goal, ?Goal0@{f:=?Goal2 fe} $== f
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: Cat_BiInv A x y
y $-> x
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: Cat_BiInv A x y
?Goal4 $o ?Goal0 $== Id x
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: Cat_BiInv A x y
?Goal0 $o ?Goal4 $== Id y
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: x $-> y
forall g : y $-> x,
f $o g $== Id y -> g $o f $== Id x -> ?Goal
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: x $-> y
Type exact (Cat_IsBiInv f).
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: Cat_BiInv A x y
x $-> y exact f.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: Cat_BiInv A x y
Cat_IsBiInv f exact _.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: x $-> y
Cat_IsBiInv f -> Cat_BiInv A x y apply Build_Cat_BiInv.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: x $-> y
forall fe : Cat_IsBiInv f,
{| cat_equiv_fun := f; cat_equiv_isequiv := fe |} $==
f intros; reflexivity.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: Cat_BiInv A x y
y $-> x exact (cat_equiv_inv f).
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: Cat_BiInv A x y
cat_equiv_inv f $o f $== Id x apply cat_eissect.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: Cat_BiInv A x y
f $o cat_equiv_inv f $== Id y apply cat_eisretr.
  -A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: x $-> y
forall g : y $-> x,
f $o g $== Id y -> g $o f $== Id x -> Cat_IsBiInv f intros g r s.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
x, y: A
f: x $-> y
g: y $-> x
r: f $o g $== Id y
s: g $o f $== Id x
Cat_IsBiInv f
    exact (Build_Cat_IsBiInv g r g s).
Defined.