{A B : Type} `{HasEquivs A} `{HasEquivs B} (F : A -> B) `{!Is0Functor F, !Is1Functor F} {a b : A} (e : a $<~> b) : cate_fun (emap F e)^-1$ $== cate_fun (emap F e^-1$). Proof. refine (cate_inv_adjointify _ _ _ _ $@ _). exact (cate_buildequiv_fun _)^$. Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.