{A B : Type} `{HasEquivs A} `{HasEquivs B} (F : A -> B) `{!Is0Functor F, !Is1Functor F} {a b c : A} (f : a $<~> b) (g : b $<~> c) : cate_fun (emap F (g $oE f)) $== fmap F (cate_fun g) $o fmap F (cate_fun f). Proof. refine (cate_buildequiv_fun _ $@ _). refine (fmap2 F (compose_cate_fun _ _) $@ _). rapply fmap_comp. Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.