{A B : Type} (F : A -> B) `{IsSurjInj A B F} : surjinj_inv F o F $=> idmap. Proof. intros a. apply (essinj F). apply eisretr0gpd_inv. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Iff. Require Import WildCat.Core. Require Import WildCat.NatTrans. Require Import WildCat.Sigma.