{A B : Type} {f : A $-> B} `{IsEquiv A B f} : CatIsEquiv f. Proof. assumption. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Equivalences Basics.PathGroupoids. Require Import Types.Equiv. Require Import WildCat.Core WildCat.Equiv WildCat.NatTrans WildCat.TwoOneCat.