{A B C : Type} `{IsGraph A, IsGraph B, IsGraph C} (F : A -> B -> C) `{!Is0Bifunctor F} {a0 a1 : A} (f : a0 $-> a1) (b : B) : (F a0 b) $-> (F a1 b) := fmap (flip F b) f.
Require Import Basics.Overture Basics.Tactics. Require Import Types.Forall Types.Prod. Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans