A `{Is1Cat A} : HasEquivs A. Proof. srapply Build_HasEquivs; intros x y. 1: exact (Cat_BiInv _ x y). all:intros f; cbn beta in *. - exact (Cat_IsBiInv f). - exact f. - exact _. - apply Build_Cat_BiInv. - intros; reflexivity. - exact (cat_equiv_inv f). - apply cat_eissect. - apply cat_eisretr. - intros g r s. exact (Build_Cat_IsBiInv g r g s). Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.