A `{Is1Cat A} (x y : A) := { cat_equiv_fun :> x $-> y; cat_equiv_isequiv : Cat_IsBiInv cat_equiv_fun; }.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.