fact: Definition cate_adjointify {A} `{HasEquivs A} {a b : A} (f : a $-> b) (g : b $-> a) (r : f $o g $== Id b) (s : g $o f $== Id a) : a $<~> b := Build_CatEquiv f (fe:=catie_adjointify f g r s).
imports: Basics.Utf8 Basics.Overture Basics.Tactics WildCat.Core