{A B C : Type} `{IsGraph A, IsGraph B, IsGraph C} (F : A -> B -> C) `{!Is0Bifunctor F} (a : A) {b0 b1 : B} (g : b0 $-> b1) : F a b0 $-> F a b1 := fmap (F a) g.
Require Import Basics.Overture Basics.Tactics. Require Import Types.Forall Types.Prod. Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans