{A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F} {a00 a20 a02 a22 : A} {f10 : a00 $-> a20} {f12 : a02 $-> a22} {f01 : a00 $-> a02} {f21 : a20 $-> a22} {b00 b20 b02 b22 : B} {g10 : b00 $-> b20} {g12 : b02 $-> b22} {g01 : b00 $-> b02} {g21 : b20 $-> b22} (p : Square f01 f21 f10 f12) (q : Square g01 g21 g10 g12) : Square (fmap11 F f01 g01) (fmap11 F f21 g21) (fmap11 F f10 g10) (fmap11 F f12 g12) := (fmap11_comp F _ _ _ _)^$ $@ fmap22 F p q $@ fmap11_comp F _ _ _ _. Global Instance is1natural_uncurry {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F} (G : A -> B -> C) `{!Is0Bifunctor G, !Is1Bifunctor G} (alpha : uncurry F $=> uncurry G) (nat_l : forall b, Is1Natural (flip F b) (flip G b) (fun x : A => alpha (x, b))) (nat_r : forall a, Is1Natural (F a) (G a) (fun y : B => alpha (a, y))) : Is1Natural (uncurry F) (uncurry G) alpha. Proof. snrapply Build_Is1Natural. intros [a b] [a' b'] [f f']; cbn in *. change (?w $o ?x $== ?y $o ?z) with (Square z w x y). nrapply vconcatL. 1: rapply (fmap11_is_fmap01_fmap10 F). nrapply vconcatR. 2: rapply (fmap11_is_fmap01_fmap10 G). exact (hconcat (nat_l _ _ _ f) (nat_r _ _ _ f')). Defined.
Require Import Basics.Overture Basics.Tactics. Require Import Types.Forall Types.Prod. Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans