`{HasEquivs B} : HasEquivs A. Proof. srapply Build_HasEquivs; intros a b; cbn. + exact (f a $<~> f b). + apply CatIsEquiv'. + apply cate_fun. + apply cate_isequiv'. + apply cate_buildequiv'. + nrapply cate_buildequiv_fun'. + apply cate_inv'. + nrapply cate_issect'. + nrapply cate_isretr'. + nrapply catie_adjointify'. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv.