{A} `{HasEquivs A} {a b : A} (f : a $-> b) `{!CatIsEquiv f} {g : a $-> b} (p : f $== g) : CatIsEquiv g. Proof. snrapply catie_adjointify. - exact (Build_CatEquiv f)^-1$. - refine (p^$ $@R _ $@ _). refine ((cate_buildequiv_fun f)^$ $@R _ $@ _). apply cate_isretr. - refine (_ $@L p^$ $@ _). refine (_ $@L (cate_buildequiv_fun f)^$ $@ _). apply cate_issect. Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.