{A} `{HasEquivs A} {a b : A} (f : a $-> b) {fe : CatIsEquiv f} : cate_fun (Build_CatEquiv f) $== f := ' a b f fe.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.