{A} `{Is1Cat A} {x y : A} (f : x $-> y) {bif : Cat_IsBiInv f} : cat_equiv_inv f $== cat_equiv_inv' f. Proof. refine ((cat_idl _)^$ $@ _). refine (cat_prewhisker (cat_eissect' f)^$ _ $@ _). refine (cat_assoc _ _ _ $@ _). refine (cat_postwhisker _ (cat_eisretr f) $@ _). apply cat_idr. Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.