{G H : ZeroGpd} (F : G $-> H) {e : IsSurjInj F} : Cat_IsBiInv F. Proof. destruct e as [e0 e1]; unfold SplEssSurj in e0. srapply catie_adjointify. - snrapply Build_Morphism_0Gpd. 1: exact (fun y => (e0 y).1). snrapply Build_Is0Functor; cbn beta. intros y1 y2 m. apply e1. exact ((e0 y1).2 $@ m $@ ((e0 y2).2)^$). - cbn. apply e0. - cbn. intro x. apply e1. apply e0. Defined.
Require Import Basics.Overture Basics.Tactics Require Import WildCat.Core WildCat.Equiv WildCat.EquivGpd