fact: Definition emap_id {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)).
imports: Basics.Utf8 Basics.Overture Basics.Tactics WildCat.Core