{A B : Type} `{HasEquivs A} `{HasEquivs B} (F : A -> B) `{!Is0Functor F, !Is1Functor F} {a : A} : cate_fun (emap F (id_cate a)) $== cate_fun (id_cate (F a)). Proof. refine (cate_buildequiv_fun _ $@ _). refine (fmap2 F (id_cate_fun a) $@ _ $@ (id_cate_fun (F a))^$). rapply fmap_id. Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.