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