Require Import Basics.Overture Basics.Tactics Basics.Iff.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.Core.
Require Import WildCat.NatTrans.
Require Import WildCat.Sigma.

(** * Equivalences of 0-groupoids, and split essentially surjective functors *)

(** For a logically equivalent definition of equivalences of 0-groupoids, see ZeroGroupoid.v. *)

(** We could define these similarly for more general categories too, but we'd need to use [HasEquivs] and [$<~>] instead of [$==]. *)

Class SplEssSurj {A B : Type} `{Is0Gpd A, Is0Gpd B}
      (F : A -> B) `{!Is0Functor F} 
  := esssurj : forall b:B, { a:A & F a $== b }.

Arguments esssurj {A B _ _ _ _ _ _} F {_ _} b.

(** A 0-functor between 0-groupoids is an "equivalence" if it is essentially surjective and reflects the existence of morphisms.  This is "surjective and injective" in setoid-language, so we use the name [IsSurjInj].  (To define essential surjectivity for non-groupoids, we would need [HasEquivs] from [WildCat.Equiv]. *)
Class IsSurjInj {A B : Type} `{Is0Gpd A, Is0Gpd B}
      (F : A -> B) `{!Is0Functor F} :=
{
  esssurj_issurjinj :: SplEssSurj F ;
  essinj : forall (x y:A), (F x $== F y) -> (x $== y) ;
}.

Arguments essinj {A B _ _ _ _ _ _} F {_ _ x y} f.

Definition surjinj_inv {A B : Type} (F : A -> B) `{IsSurjInj A B F} : B -> A
  := fun b => (esssurj F b).1.

(** Some of the results below also follow from the logical equivalence with [IsEquiv_0Gpd] and the fact that [ZeroGpd] satisfies [HasEquivs].  But it is sometimes awkward to deduce the results this way, mostly because [ZeroGpd] requires bundled objects rather than typeclass instances. *)

(** Equivalences have inverses *)

Instance is0functor_surjinj_inv
       {A B : Type} (F : A -> B) `{IsSurjInj A B F}
  : Is0Functor (surjinj_inv F).
A, B: Type
F: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
Is0Functor (surjinj_inv F)
Proof.
A, B: Type
F: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
Is0Functor (surjinj_inv F)
  constructor; intros x y f.
A, B: Type
F: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
x, y: B
f: x $-> y
surjinj_inv F x $-> surjinj_inv F y
  pose (p := (esssurj F x).2).
A, B: Type
F: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
x, y: B
f: x $-> y
p:= (esssurj F x).2: (fun a : A => F a $== x) (esssurj F x).1
surjinj_inv F x $-> surjinj_inv F y
  pose (q := (esssurj F y).2).
A, B: Type
F: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
x, y: B
f: x $-> y
p:= (esssurj F x).2: (fun a : A => F a $== x) (esssurj F x).1
q:= (esssurj F y).2: (fun a : A => F a $== y) (esssurj F y).1
surjinj_inv F x $-> surjinj_inv F y
  cbn in *.
A, B: Type
F: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
x, y: B
f: x $-> y
p:= (esssurj F x).2: F (esssurj F x).1 $== x
q:= (esssurj F y).2: F (esssurj F y).1 $== y
surjinj_inv F x $-> surjinj_inv F y
  pose (f' := p $@ f $@ q^$).
A, B: Type
F: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
x, y: B
f: x $-> y
p:= (esssurj F x).2: F (esssurj F x).1 $== x
q:= (esssurj F y).2: F (esssurj F y).1 $== y
f':= (p $@ f) $@ q^$: F (esssurj F x).1 $== F (esssurj F y).1
surjinj_inv F x $-> surjinj_inv F y
  exact (essinj F f').
Defined.

(** The inverse is an inverse, up to unnatural transformations *)

Definition eisretr0gpd_inv {A B : Type} (F : A -> B) `{IsSurjInj A B F}
  : F o surjinj_inv F $=> idmap.
A, B: Type
F: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
F o surjinj_inv F $=> idmap
Proof.
A, B: Type
F: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
F o surjinj_inv F $=> idmap
  intros b.
A, B: Type
F: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
b: B
F (surjinj_inv F b) $-> b
  exact ((esssurj F b).2).
Defined.

Definition eissect0gpd_inv {A B : Type} (F : A -> B) `{IsSurjInj A B F}
  : surjinj_inv F o F $=> idmap.
A, B: Type
F: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
surjinj_inv F o F $=> idmap
Proof.
A, B: Type
F: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
surjinj_inv F o F $=> idmap
  intros a.
A, B: Type
F: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
a: A
surjinj_inv F (F a) $-> a
  apply (essinj F).
A, B: Type
F: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
a: A
F (surjinj_inv F (F a)) $== F a
  apply eisretr0gpd_inv.
Defined.

(** Essentially surjective functors and equivalences are preserved by transformations. *)
Definition isesssurj_transf {A B : Type} {F : A -> B} {G : A -> B}
           `{SplEssSurj A B F} `{!Is0Functor G} (alpha : G $=> F)
  : SplEssSurj G.
A, B: Type
F, G: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: SplEssSurj F
Is0Functor1: Is0Functor G
alpha: G $=> F
SplEssSurj G
Proof.
A, B: Type
F, G: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: SplEssSurj F
Is0Functor1: Is0Functor G
alpha: G $=> F
SplEssSurj G
  intros b.
A, B: Type
F, G: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: SplEssSurj F
Is0Functor1: Is0Functor G
alpha: G $=> F
b: B
{a : A & G a $== b}
  exists ((esssurj F b).1).
A, B: Type
F, G: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: SplEssSurj F
Is0Functor1: Is0Functor G
alpha: G $=> F
b: B
G (esssurj F b).1 $== b
  refine (_ $@ (esssurj F b).2).
A, B: Type
F, G: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: SplEssSurj F
Is0Functor1: Is0Functor G
alpha: G $=> F
b: B
G (esssurj F b).1 $== F (esssurj F b).1
  apply alpha.
Defined.

Definition issurjinj_transf {A B : Type} {F : A -> B} {G : A -> B}
           `{IsSurjInj A B F} `{!Is0Functor G} (alpha : G $=> F)
  : IsSurjInj G.
A, B: Type
F, G: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
Is0Functor1: Is0Functor G
alpha: G $=> F
IsSurjInj G
Proof.
A, B: Type
F, G: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
Is0Functor1: Is0Functor G
alpha: G $=> F
IsSurjInj G
  constructor.
A, B: Type
F, G: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
Is0Functor1: Is0Functor G
alpha: G $=> F
SplEssSurj G
A, B: Type
F, G: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
Is0Functor1: Is0Functor G
alpha: G $=> F
forall x y : A, G x $== G y -> x $== y
  -
A, B: Type
F, G: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
Is0Functor1: Is0Functor G
alpha: G $=> F
SplEssSurj G exact (isesssurj_transf alpha).
  -
A, B: Type
F, G: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
Is0Functor1: Is0Functor G
alpha: G $=> F
forall x y : A, G x $== G y -> x $== y intros x y f.
A, B: Type
F, G: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
Is0Functor1: Is0Functor G
alpha: G $=> F
x, y: A
f: G x $== G y
x $== y
    apply (essinj F).
A, B: Type
F, G: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
Is0Functor1: Is0Functor G
alpha: G $=> F
x, y: A
f: G x $== G y
F x $== F y
    refine (_ $@ f $@ _).
A, B: Type
F, G: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
Is0Functor1: Is0Functor G
alpha: G $=> F
x, y: A
f: G x $== G y
F x $== G x
A, B: Type
F, G: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
Is0Functor1: Is0Functor G
alpha: G $=> F
x, y: A
f: G x $== G y
G y $== F y
    +
A, B: Type
F, G: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
Is0Functor1: Is0Functor G
alpha: G $=> F
x, y: A
f: G x $== G y
F x $== G x symmetry; apply alpha.
    +
A, B: Type
F, G: A -> B
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Functor0: Is0Functor F
H5: IsSurjInj F
Is0Functor1: Is0Functor G
alpha: G $=> F
x, y: A
f: G x $== G y
G y $== F y apply alpha.
Defined.

(** Equivalences compose and cancel with each other and with essentially surjective functors. *)

Section ComposeAndCancel.
  Context {A B C} `{Is0Gpd A, Is0Gpd B, Is0Gpd C}
       (G : B -> C) (F : A -> B) `{!Is0Functor G, !Is0Functor F}.

  #[export] Instance isesssurj_compose
         `{!SplEssSurj G, !SplEssSurj F}
    : SplEssSurj (G o F).
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
SplEssSurj0: SplEssSurj G
SplEssSurj1: SplEssSurj F
SplEssSurj (G o F)
  Proof.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
SplEssSurj0: SplEssSurj G
SplEssSurj1: SplEssSurj F
SplEssSurj (G o F)
    intros c.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
SplEssSurj0: SplEssSurj G
SplEssSurj1: SplEssSurj F
c: C
{a : A & G (F a) $== c}
    exists ((esssurj F (esssurj G c).1).1).
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
SplEssSurj0: SplEssSurj G
SplEssSurj1: SplEssSurj F
c: C
G (F (esssurj F (esssurj G c).1).1) $== c
    refine (_ $@ (esssurj G c).2).
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
SplEssSurj0: SplEssSurj G
SplEssSurj1: SplEssSurj F
c: C
G (F (esssurj F (esssurj G c).1).1) $==
G (esssurj G c).1
    apply (fmap G).
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
SplEssSurj0: SplEssSurj G
SplEssSurj1: SplEssSurj F
c: C
F (esssurj F (esssurj G c).1).1 $-> (esssurj G c).1
    apply (esssurj F).
  Defined.

  #[export] Instance issurjinj_compose
         `{!IsSurjInj G, !IsSurjInj F}
    : IsSurjInj (G o F).
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
IsSurjInj1: IsSurjInj F
IsSurjInj (G o F)
  Proof.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
IsSurjInj1: IsSurjInj F
IsSurjInj (G o F)
    constructor.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
IsSurjInj1: IsSurjInj F
SplEssSurj (fun x : A => G (F x))
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
IsSurjInj1: IsSurjInj F
forall x y : A, G (F x) $== G (F y) -> x $== y
    -
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
IsSurjInj1: IsSurjInj F
SplEssSurj (fun x : A => G (F x)) exact _.
    -
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
IsSurjInj1: IsSurjInj F
forall x y : A, G (F x) $== G (F y) -> x $== y intros x y f.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
IsSurjInj1: IsSurjInj F
x, y: A
f: G (F x) $== G (F y)
x $== y
      apply (essinj F).
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
IsSurjInj1: IsSurjInj F
x, y: A
f: G (F x) $== G (F y)
F x $== F y
      exact (essinj G f).
  Defined.

  Definition cancelL_isesssurj
             `{!IsSurjInj G, !SplEssSurj (G o F)}
    : SplEssSurj F.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
SplEssSurj0: SplEssSurj (G o F)
SplEssSurj F
  Proof.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
SplEssSurj0: SplEssSurj (G o F)
SplEssSurj F
    intros b.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
SplEssSurj0: SplEssSurj (G o F)
b: B
{a : A & F a $== b}
    exists ((esssurj (G o F) (G b)).1).
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
SplEssSurj0: SplEssSurj (G o F)
b: B
F (esssurj (fun x : A => G (F x)) (G b)).1 $== b
    apply (essinj G).
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
SplEssSurj0: SplEssSurj (G o F)
b: B
G (F (esssurj (fun x : A => G (F x)) (G b)).1) $== G b
    exact ((esssurj (G o F) (G b)).2).
  Defined.

  Definition iffL_isesssurj `{!IsSurjInj G}
    : SplEssSurj (G o F) <-> SplEssSurj F.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
SplEssSurj (G o F) <-> SplEssSurj F
  Proof.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
SplEssSurj (G o F) <-> SplEssSurj F
    split; [ apply @cancelL_isesssurj | apply @isesssurj_compose ]; exact _.
  Defined.

  Definition cancelL_issurjinj
             `{!IsSurjInj G, !IsSurjInj (G o F)}
    : IsSurjInj F.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
IsSurjInj1: IsSurjInj (G o F)
IsSurjInj F
  Proof.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
IsSurjInj1: IsSurjInj (G o F)
IsSurjInj F
    constructor.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
IsSurjInj1: IsSurjInj (G o F)
SplEssSurj F
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
IsSurjInj1: IsSurjInj (G o F)
forall x y : A, F x $== F y -> x $== y
    -
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
IsSurjInj1: IsSurjInj (G o F)
SplEssSurj F exact cancelL_isesssurj.
    -
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
IsSurjInj1: IsSurjInj (G o F)
forall x y : A, F x $== F y -> x $== y intros x y f.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
IsSurjInj1: IsSurjInj (G o F)
x, y: A
f: F x $== F y
x $== y
      exact (essinj (G o F) (fmap G f)).
  Defined.

  Definition iffL_issurjinj `{!IsSurjInj G}
    : IsSurjInj (G o F) <-> IsSurjInj F.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
IsSurjInj (G o F) <-> IsSurjInj F
  Proof.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj G
IsSurjInj (G o F) <-> IsSurjInj F
    split; [ apply @cancelL_issurjinj | apply @issurjinj_compose ]; exact _.
  Defined.

  Definition cancelR_isesssurj `{!SplEssSurj (G o F)}
    : SplEssSurj G.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
SplEssSurj0: SplEssSurj (G o F)
SplEssSurj G
  Proof.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
SplEssSurj0: SplEssSurj (G o F)
SplEssSurj G
    intros c.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
SplEssSurj0: SplEssSurj (G o F)
c: C
{a : B & G a $== c}
    exists (F (esssurj (G o F) c).1).
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
SplEssSurj0: SplEssSurj (G o F)
c: C
G (F (esssurj (fun x : A => G (F x)) c).1) $== c
    exact ((esssurj (G o F) c).2).
  Defined.

  Definition iffR_isesssurj `{!SplEssSurj F}
    : SplEssSurj (G o F) <-> SplEssSurj G.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
SplEssSurj0: SplEssSurj F
SplEssSurj (G o F) <-> SplEssSurj G
  Proof.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
SplEssSurj0: SplEssSurj F
SplEssSurj (G o F) <-> SplEssSurj G
    split; [ apply @cancelR_isesssurj | intros; apply @isesssurj_compose ]; exact _.
  Defined.

  Definition cancelR_issurjinj
             `{!IsSurjInj F, !IsSurjInj (G o F)}
    : IsSurjInj G.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj1: IsSurjInj (G o F)
IsSurjInj G
  Proof.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj1: IsSurjInj (G o F)
IsSurjInj G
    constructor.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj1: IsSurjInj (G o F)
SplEssSurj G
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj1: IsSurjInj (G o F)
forall x y : B, G x $== G y -> x $== y
    -
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj1: IsSurjInj (G o F)
SplEssSurj G exact cancelR_isesssurj.
    -
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj1: IsSurjInj (G o F)
forall x y : B, G x $== G y -> x $== y intros x y f.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj1: IsSurjInj (G o F)
x, y: B
f: G x $== G y
x $== y
      pose (p := (esssurj F x).2).
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj1: IsSurjInj (G o F)
x, y: B
f: G x $== G y
p:= (esssurj F x).2: (fun a : A => F a $== x) (esssurj F x).1
x $== y
      pose (q := (esssurj F y).2).
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj1: IsSurjInj (G o F)
x, y: B
f: G x $== G y
p:= (esssurj F x).2: (fun a : A => F a $== x) (esssurj F x).1
q:= (esssurj F y).2: (fun a : A => F a $== y) (esssurj F y).1
x $== y
      cbn in *.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj1: IsSurjInj (fun x : A => G (F x))
x, y: B
f: G x $== G y
p:= (esssurj F x).2: F (esssurj F x).1 $== x
q:= (esssurj F y).2: F (esssurj F y).1 $== y
x $== y
      refine (p^$ $@ _ $@ q).
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj1: IsSurjInj (fun x : A => G (F x))
x, y: B
f: G x $== G y
p:= (esssurj F x).2: F (esssurj F x).1 $== x
q:= (esssurj F y).2: F (esssurj F y).1 $== y
F (esssurj F x).1 $== F (esssurj F y).1
      apply (fmap F).
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj1: IsSurjInj (fun x : A => G (F x))
x, y: B
f: G x $== G y
p:= (esssurj F x).2: F (esssurj F x).1 $== x
q:= (esssurj F y).2: F (esssurj F y).1 $== y
(esssurj F x).1 $-> (esssurj F y).1
      apply (essinj (G o F)).
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj1: IsSurjInj (fun x : A => G (F x))
x, y: B
f: G x $== G y
p:= (esssurj F x).2: F (esssurj F x).1 $== x
q:= (esssurj F y).2: F (esssurj F y).1 $== y
G (F (esssurj F x).1) $== G (F (esssurj F y).1)
      refine (_ $@ f $@ _).
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj1: IsSurjInj (fun x : A => G (F x))
x, y: B
f: G x $== G y
p:= (esssurj F x).2: F (esssurj F x).1 $== x
q:= (esssurj F y).2: F (esssurj F y).1 $== y
G (F (esssurj F x).1) $== G x
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj1: IsSurjInj (fun x : A => G (F x))
x, y: B
f: G x $== G y
p:= (esssurj F x).2: F (esssurj F x).1 $== x
q:= (esssurj F y).2: F (esssurj F y).1 $== y
G y $== G (F (esssurj F y).1)
      +
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj1: IsSurjInj (fun x : A => G (F x))
x, y: B
f: G x $== G y
p:= (esssurj F x).2: F (esssurj F x).1 $== x
q:= (esssurj F y).2: F (esssurj F y).1 $== y
G (F (esssurj F x).1) $== G x exact (fmap G p).
      +
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj1: IsSurjInj (fun x : A => G (F x))
x, y: B
f: G x $== G y
p:= (esssurj F x).2: F (esssurj F x).1 $== x
q:= (esssurj F y).2: F (esssurj F y).1 $== y
G y $== G (F (esssurj F y).1) exact (fmap G q^$).
  Defined.

  Definition iffR_issurjinj `{!IsSurjInj F}
    : IsSurjInj (G o F) <-> IsSurjInj G.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj (G o F) <-> IsSurjInj G
  Proof.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
H5: IsGraph C
H6: Is01Cat C
H7: Is0Gpd C
G: B -> C
F: A -> B
Is0Functor0: Is0Functor G
Is0Functor1: Is0Functor F
IsSurjInj0: IsSurjInj F
IsSurjInj (G o F) <-> IsSurjInj G
    split; [ apply @cancelR_issurjinj | intros; apply @issurjinj_compose ]; exact _.
  Defined.

End ComposeAndCancel.

(** In particular, essential surjectivity and being an equivalence transfer across commutative squares of functors. *)
Definition isesssurj_iff_commsq {A B C D : Type}
           {F : A -> B} {G : C -> D} {H : A -> C} {K : B -> D}
           `{IsSurjInj A C H} `{IsSurjInj B D K}
           `{!Is0Functor F} `{!Is0Functor G}
           (p : K o F $=> G o H)
  : SplEssSurj F <-> SplEssSurj G.
A, B, C, D: Type
F: A -> B
G: C -> D
H: A -> C
K: B -> D
H0: IsGraph A
H1: Is01Cat A
H2: Is0Gpd A
H3: IsGraph C
H4: Is01Cat C
H5: Is0Gpd C
Is0Functor0: Is0Functor H
H6: IsSurjInj H
H7: IsGraph B
H8: Is01Cat B
H9: Is0Gpd B
H10: IsGraph D
H11: Is01Cat D
H12: Is0Gpd D
Is0Functor1: Is0Functor K
H13: IsSurjInj K
Is0Functor2: Is0Functor F
Is0Functor3: Is0Functor G
p: K o F $=> G o H
SplEssSurj F <-> SplEssSurj G
Proof.
A, B, C, D: Type
F: A -> B
G: C -> D
H: A -> C
K: B -> D
H0: IsGraph A
H1: Is01Cat A
H2: Is0Gpd A
H3: IsGraph C
H4: Is01Cat C
H5: Is0Gpd C
Is0Functor0: Is0Functor H
H6: IsSurjInj H
H7: IsGraph B
H8: Is01Cat B
H9: Is0Gpd B
H10: IsGraph D
H11: Is01Cat D
H12: Is0Gpd D
Is0Functor1: Is0Functor K
H13: IsSurjInj K
Is0Functor2: Is0Functor F
Is0Functor3: Is0Functor G
p: K o F $=> G o H
SplEssSurj F <-> SplEssSurj G
  split; intros ?.
A, B, C, D: Type
F: A -> B
G: C -> D
H: A -> C
K: B -> D
H0: IsGraph A
H1: Is01Cat A
H2: Is0Gpd A
H3: IsGraph C
H4: Is01Cat C
H5: Is0Gpd C
Is0Functor0: Is0Functor H
H6: IsSurjInj H
H7: IsGraph B
H8: Is01Cat B
H9: Is0Gpd B
H10: IsGraph D
H11: Is01Cat D
H12: Is0Gpd D
Is0Functor1: Is0Functor K
H13: IsSurjInj K
Is0Functor2: Is0Functor F
Is0Functor3: Is0Functor G
p: K o F $=> G o H
X: SplEssSurj F
SplEssSurj G
A, B, C, D: Type
F: A -> B
G: C -> D
H: A -> C
K: B -> D
H0: IsGraph A
H1: Is01Cat A
H2: Is0Gpd A
H3: IsGraph C
H4: Is01Cat C
H5: Is0Gpd C
Is0Functor0: Is0Functor H
H6: IsSurjInj H
H7: IsGraph B
H8: Is01Cat B
H9: Is0Gpd B
H10: IsGraph D
H11: Is01Cat D
H12: Is0Gpd D
Is0Functor1: Is0Functor K
H13: IsSurjInj K
Is0Functor2: Is0Functor F
Is0Functor3: Is0Functor G
p: K o F $=> G o H
X: SplEssSurj G
SplEssSurj F
  -
A, B, C, D: Type
F: A -> B
G: C -> D
H: A -> C
K: B -> D
H0: IsGraph A
H1: Is01Cat A
H2: Is0Gpd A
H3: IsGraph C
H4: Is01Cat C
H5: Is0Gpd C
Is0Functor0: Is0Functor H
H6: IsSurjInj H
H7: IsGraph B
H8: Is01Cat B
H9: Is0Gpd B
H10: IsGraph D
H11: Is01Cat D
H12: Is0Gpd D
Is0Functor1: Is0Functor K
H13: IsSurjInj K
Is0Functor2: Is0Functor F
Is0Functor3: Is0Functor G
p: K o F $=> G o H
X: SplEssSurj F
SplEssSurj G srapply (cancelR_isesssurj G H); try exact _.
A, B, C, D: Type
F: A -> B
G: C -> D
H: A -> C
K: B -> D
H0: IsGraph A
H1: Is01Cat A
H2: Is0Gpd A
H3: IsGraph C
H4: Is01Cat C
H5: Is0Gpd C
Is0Functor0: Is0Functor H
H6: IsSurjInj H
H7: IsGraph B
H8: Is01Cat B
H9: Is0Gpd B
H10: IsGraph D
H11: Is01Cat D
H12: Is0Gpd D
Is0Functor1: Is0Functor K
H13: IsSurjInj K
Is0Functor2: Is0Functor F
Is0Functor3: Is0Functor G
p: K o F $=> G o H
X: SplEssSurj F
SplEssSurj (G o H)
    exact (isesssurj_transf (fun a => (p a)^$)).
  -
A, B, C, D: Type
F: A -> B
G: C -> D
H: A -> C
K: B -> D
H0: IsGraph A
H1: Is01Cat A
H2: Is0Gpd A
H3: IsGraph C
H4: Is01Cat C
H5: Is0Gpd C
Is0Functor0: Is0Functor H
H6: IsSurjInj H
H7: IsGraph B
H8: Is01Cat B
H9: Is0Gpd B
H10: IsGraph D
H11: Is01Cat D
H12: Is0Gpd D
Is0Functor1: Is0Functor K
H13: IsSurjInj K
Is0Functor2: Is0Functor F
Is0Functor3: Is0Functor G
p: K o F $=> G o H
X: SplEssSurj G
SplEssSurj F srapply (cancelL_isesssurj K F); try exact _.
A, B, C, D: Type
F: A -> B
G: C -> D
H: A -> C
K: B -> D
H0: IsGraph A
H1: Is01Cat A
H2: Is0Gpd A
H3: IsGraph C
H4: Is01Cat C
H5: Is0Gpd C
Is0Functor0: Is0Functor H
H6: IsSurjInj H
H7: IsGraph B
H8: Is01Cat B
H9: Is0Gpd B
H10: IsGraph D
H11: Is01Cat D
H12: Is0Gpd D
Is0Functor1: Is0Functor K
H13: IsSurjInj K
Is0Functor2: Is0Functor F
Is0Functor3: Is0Functor G
p: K o F $=> G o H
X: SplEssSurj G
SplEssSurj (K o F)
    exact (isesssurj_transf p).
Defined.

Definition issurjinj_iff_commsq {A B C D : Type}
           {F : A -> B} {G : C -> D} {H : A -> C} {K : B -> D}
           `{IsSurjInj A C H} `{IsSurjInj B D K}
           `{!Is0Functor F} `{!Is0Functor G}
           (p : K o F $=> G o H)
  : IsSurjInj F <-> IsSurjInj G.
A, B, C, D: Type
F: A -> B
G: C -> D
H: A -> C
K: B -> D
H0: IsGraph A
H1: Is01Cat A
H2: Is0Gpd A
H3: IsGraph C
H4: Is01Cat C
H5: Is0Gpd C
Is0Functor0: Is0Functor H
H6: IsSurjInj H
H7: IsGraph B
H8: Is01Cat B
H9: Is0Gpd B
H10: IsGraph D
H11: Is01Cat D
H12: Is0Gpd D
Is0Functor1: Is0Functor K
H13: IsSurjInj K
Is0Functor2: Is0Functor F
Is0Functor3: Is0Functor G
p: K o F $=> G o H
IsSurjInj F <-> IsSurjInj G
Proof.
A, B, C, D: Type
F: A -> B
G: C -> D
H: A -> C
K: B -> D
H0: IsGraph A
H1: Is01Cat A
H2: Is0Gpd A
H3: IsGraph C
H4: Is01Cat C
H5: Is0Gpd C
Is0Functor0: Is0Functor H
H6: IsSurjInj H
H7: IsGraph B
H8: Is01Cat B
H9: Is0Gpd B
H10: IsGraph D
H11: Is01Cat D
H12: Is0Gpd D
Is0Functor1: Is0Functor K
H13: IsSurjInj K
Is0Functor2: Is0Functor F
Is0Functor3: Is0Functor G
p: K o F $=> G o H
IsSurjInj F <-> IsSurjInj G
  split; intros ?.
A, B, C, D: Type
F: A -> B
G: C -> D
H: A -> C
K: B -> D
H0: IsGraph A
H1: Is01Cat A
H2: Is0Gpd A
H3: IsGraph C
H4: Is01Cat C
H5: Is0Gpd C
Is0Functor0: Is0Functor H
H6: IsSurjInj H
H7: IsGraph B
H8: Is01Cat B
H9: Is0Gpd B
H10: IsGraph D
H11: Is01Cat D
H12: Is0Gpd D
Is0Functor1: Is0Functor K
H13: IsSurjInj K
Is0Functor2: Is0Functor F
Is0Functor3: Is0Functor G
p: K o F $=> G o H
X: IsSurjInj F
IsSurjInj G
A, B, C, D: Type
F: A -> B
G: C -> D
H: A -> C
K: B -> D
H0: IsGraph A
H1: Is01Cat A
H2: Is0Gpd A
H3: IsGraph C
H4: Is01Cat C
H5: Is0Gpd C
Is0Functor0: Is0Functor H
H6: IsSurjInj H
H7: IsGraph B
H8: Is01Cat B
H9: Is0Gpd B
H10: IsGraph D
H11: Is01Cat D
H12: Is0Gpd D
Is0Functor1: Is0Functor K
H13: IsSurjInj K
Is0Functor2: Is0Functor F
Is0Functor3: Is0Functor G
p: K o F $=> G o H
X: IsSurjInj G
IsSurjInj F
  -
A, B, C, D: Type
F: A -> B
G: C -> D
H: A -> C
K: B -> D
H0: IsGraph A
H1: Is01Cat A
H2: Is0Gpd A
H3: IsGraph C
H4: Is01Cat C
H5: Is0Gpd C
Is0Functor0: Is0Functor H
H6: IsSurjInj H
H7: IsGraph B
H8: Is01Cat B
H9: Is0Gpd B
H10: IsGraph D
H11: Is01Cat D
H12: Is0Gpd D
Is0Functor1: Is0Functor K
H13: IsSurjInj K
Is0Functor2: Is0Functor F
Is0Functor3: Is0Functor G
p: K o F $=> G o H
X: IsSurjInj F
IsSurjInj G srapply (cancelR_issurjinj G H); try exact _.
A, B, C, D: Type
F: A -> B
G: C -> D
H: A -> C
K: B -> D
H0: IsGraph A
H1: Is01Cat A
H2: Is0Gpd A
H3: IsGraph C
H4: Is01Cat C
H5: Is0Gpd C
Is0Functor0: Is0Functor H
H6: IsSurjInj H
H7: IsGraph B
H8: Is01Cat B
H9: Is0Gpd B
H10: IsGraph D
H11: Is01Cat D
H12: Is0Gpd D
Is0Functor1: Is0Functor K
H13: IsSurjInj K
Is0Functor2: Is0Functor F
Is0Functor3: Is0Functor G
p: K o F $=> G o H
X: IsSurjInj F
IsSurjInj (G o H)
    exact (issurjinj_transf (fun a => (p a)^$)).
  -
A, B, C, D: Type
F: A -> B
G: C -> D
H: A -> C
K: B -> D
H0: IsGraph A
H1: Is01Cat A
H2: Is0Gpd A
H3: IsGraph C
H4: Is01Cat C
H5: Is0Gpd C
Is0Functor0: Is0Functor H
H6: IsSurjInj H
H7: IsGraph B
H8: Is01Cat B
H9: Is0Gpd B
H10: IsGraph D
H11: Is01Cat D
H12: Is0Gpd D
Is0Functor1: Is0Functor K
H13: IsSurjInj K
Is0Functor2: Is0Functor F
Is0Functor3: Is0Functor G
p: K o F $=> G o H
X: IsSurjInj G
IsSurjInj F srapply (cancelL_issurjinj K F); try exact _.
A, B, C, D: Type
F: A -> B
G: C -> D
H: A -> C
K: B -> D
H0: IsGraph A
H1: Is01Cat A
H2: Is0Gpd A
H3: IsGraph C
H4: Is01Cat C
H5: Is0Gpd C
Is0Functor0: Is0Functor H
H6: IsSurjInj H
H7: IsGraph B
H8: Is01Cat B
H9: Is0Gpd B
H10: IsGraph D
H11: Is01Cat D
H12: Is0Gpd D
Is0Functor1: Is0Functor K
H13: IsSurjInj K
Is0Functor2: Is0Functor F
Is0Functor3: Is0Functor G
p: K o F $=> G o H
X: IsSurjInj G
IsSurjInj (K o F)
    exact (issurjinj_transf p).
Defined.

(** Equivalences and essential surjectivity are preserved by sigmas (for now, just over constant bases), and essential surjectivity at least is also reflected. *)

Definition isesssurj_iff_sigma {A : Type} (B C : A -> Type)
 `{forall a, IsGraph (B a)} `{forall a, Is01Cat (B a)} `{forall a, Is0Gpd (B a)}
 `{forall a, IsGraph (C a)} `{forall a, Is01Cat (C a)} `{forall a, Is0Gpd (C a)}
  (F : forall a, B a -> C a) {ff : forall a, Is0Functor (F a)}
  : SplEssSurj (fun (x:sig B) => (x.1 ; F x.1 x.2))
    <-> (forall a, SplEssSurj (F a)).
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
SplEssSurj (fun x : {x : _ & B x} => (x.1; F x.1 x.2)) <->
(forall a : A, SplEssSurj (F a))
Proof.
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
SplEssSurj (fun x : {x : _ & B x} => (x.1; F x.1 x.2)) <->
(forall a : A, SplEssSurj (F a))
  split.
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
SplEssSurj (fun x : {x : _ & B x} => (x.1; F x.1 x.2)) ->
forall a : A, SplEssSurj (F a)
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
(forall a : A, SplEssSurj (F a)) ->
SplEssSurj (fun x : {x : _ & B x} => (x.1; F x.1 x.2))
  -
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
SplEssSurj (fun x : {x : _ & B x} => (x.1; F x.1 x.2)) ->
forall a : A, SplEssSurj (F a) intros fs a c.
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
fs: SplEssSurj
  (fun x : {x : _ & B x} => (x.1; F x.1 x.2))
a: A
c: C a
{a0 : B a & F a a0 $== c}
    pose (s := fs (a;c)).
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
fs: SplEssSurj
  (fun x : {x : _ & B x} => (x.1; F x.1 x.2))
a: A
c: C a
s:= fs (a; c): {a0 : {x : _ & B x} &
(fun x : {x : _ & B x} => (x.1; F x.1 x.2)) a0 $==
(a; c)}
{a0 : B a & F a a0 $== c}
    destruct s as [[a' b] [p q]]; cbn in *.
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
fs: SplEssSurj
  (fun x : {x : _ & B x} => (x.1; F x.1 x.2))
a: A
c: C a
a': A
b: B a'
p: a' = a
q: transport C p (F a' b) $-> c
{a0 : B a & F a a0 $== c}
    destruct p; cbn in q.
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
fs: SplEssSurj
  (fun x : {x : _ & B x} => (x.1; F x.1 x.2))
a': A
c: C a'
b: B a'
q: F a' b $-> c
{a : B a' & F a' a $== c}
    exists b.
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
fs: SplEssSurj
  (fun x : {x : _ & B x} => (x.1; F x.1 x.2))
a': A
c: C a'
b: B a'
q: F a' b $-> c
F a' b $== c
    exact q.
  -
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
(forall a : A, SplEssSurj (F a)) ->
SplEssSurj (fun x : {x : _ & B x} => (x.1; F x.1 x.2)) intros fs [a c].
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
fs: forall a : A, SplEssSurj (F a)
a: A
c: C a
{a0 : {x : _ & B x} & (a0.1; F a0.1 a0.2) $== (a; c)}
    exists (a ; (esssurj (F a) c).1); cbn.
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
fs: forall a : A, SplEssSurj (F a)
a: A
c: C a
{p : a = a &
transport C p (F a (esssurj (F a) c).1) $-> c}
    exists idpath; cbn.
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
fs: forall a : A, SplEssSurj (F a)
a: A
c: C a
F a (esssurj (F a) c).1 $-> c
    exact ((esssurj (F a) c).2).
Defined.

Definition issurjinj_sigma {A : Type} (B C : A -> Type)
 `{forall a, IsGraph (B a)} `{forall a, Is01Cat (B a)} `{forall a, Is0Gpd (B a)}
 `{forall a, IsGraph (C a)} `{forall a, Is01Cat (C a)} `{forall a, Is0Gpd (C a)}
  (F : forall a, B a -> C a)
  `{forall a, Is0Functor (F a)} `{forall a, IsSurjInj (F a)}
  : IsSurjInj (fun (x:sig B) => (x.1 ; F x.1 x.2)).
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
H5: forall a : A, Is0Functor (F a)
H6: forall a : A, IsSurjInj (F a)
IsSurjInj (fun x : {x : _ & B x} => (x.1; F x.1 x.2))
Proof.
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
H5: forall a : A, Is0Functor (F a)
H6: forall a : A, IsSurjInj (F a)
IsSurjInj (fun x : {x : _ & B x} => (x.1; F x.1 x.2))
  constructor.
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
H5: forall a : A, Is0Functor (F a)
H6: forall a : A, IsSurjInj (F a)
SplEssSurj (fun x : {x : _ & B x} => (x.1; F x.1 x.2))
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
H5: forall a : A, Is0Functor (F a)
H6: forall a : A, IsSurjInj (F a)
forall (x : {x : _ & B x}) (y : {x : _ & B x}),
(x.1; F x.1 x.2) $== (y.1; F y.1 y.2) -> x $== y
  -
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
H5: forall a : A, Is0Functor (F a)
H6: forall a : A, IsSurjInj (F a)
SplEssSurj (fun x : {x : _ & B x} => (x.1; F x.1 x.2)) apply isesssurj_iff_sigma; exact _.
  -
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
H5: forall a : A, Is0Functor (F a)
H6: forall a : A, IsSurjInj (F a)
forall (x : {x : _ & B x}) (y : {x : _ & B x}),
(x.1; F x.1 x.2) $== (y.1; F y.1 y.2) -> x $== y intros [a1 b1] [a2 b2] [p f]; cbn in *.
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
H5: forall a : A, Is0Functor (F a)
H6: forall a : A, IsSurjInj (F a)
a1: A
b1: B a1
a2: A
b2: B a2
p: a1 = a2
f: transport C p (F a1 b1) $-> F a2 b2
{p : a1 = a2 & transport B p b1 $-> b2}
    destruct p; cbn in *.
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
H5: forall a : A, Is0Functor (F a)
H6: forall a : A, IsSurjInj (F a)
a1: A
b1, b2: B a1
f: F a1 b1 $-> F a1 b2
{p : a1 = a1 & transport B p b1 $-> b2}
    exists idpath; cbn.
A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
H2: forall a : A, IsGraph (C a)
H3: forall a : A, Is01Cat (C a)
H4: forall a : A, Is0Gpd (C a)
F: forall a : A, B a -> C a
H5: forall a : A, Is0Functor (F a)
H6: forall a : A, IsSurjInj (F a)
a1: A
b1, b2: B a1
f: F a1 b1 $-> F a1 b2
b1 $-> b2
    exact (essinj (F a1) f).
Defined.