{A B} `{Is1Gpd A, Is1Gpd B} (F : A -> B) `{!Is0Functor F, !Is1Functor F} {a0 a1 : A} (f : a0 $== a1) : fmap F f^$ $== (fmap F f)^$. Proof. apply gpd_moveL_1V. refine ((fmap_comp _ _ _)^$ $@ _ $@ fmap_id _ _). rapply fmap2. apply gpd_issect. Defined.
Require Import Basics.Overture Basics.Tactics.