{A B : Type} (F : A -> B) `{IsSurjInj A B F} : B -> A := fun b => (esssurj F b).1. Global Instance is0functor_surjinj_inv {A B : Type} (F : A -> B) `{IsSurjInj A B F} : Is0Functor ( F). Proof. constructor; intros x y f. pose (p := (esssurj F x).2). pose (q := (esssurj F y).2). cbn in *. pose (f' := p $@ f $@ q^$). exact (essinj F f'). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Iff. Require Import WildCat.Core. Require Import WildCat.NatTrans. Require Import WildCat.Sigma.