{A B C : Type} (F : A -> B -> C) `{Is1Bifunctor A B C F} {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1) : fmap01 F a1 g $o fmap10 F f b0 $== fmap10 F f b1 $o fmap01 F a0 g := (fmap11_is_fmap01_fmap10 _ _ _)^$ $@ fmap11_is_fmap10_fmap01 _ _ _.
Require Import Basics.Overture Basics.Tactics. Require Import Types.Forall Types.Prod. Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans