{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} : NatTrans (uncurry F) (uncurry G) -> NatTrans (uncurry (flip F)) (uncurry (flip G)). Proof. intros alpha. snrapply Build_NatTrans. - exact (alpha o equiv_prod_symm _ _). - snrapply Build_Is1Natural'. + intros [b a] [b' a'] [g f]. exact (isnat (a:=(a, b)) (a':=(a', b')) alpha (f, g)). + intros [b a] [b' a'] [g f]. exact (isnat_tr (a:=(a, b)) (a':=(a', b')) alpha (f, g)). Defined.
Require Import Basics.Overture Basics.Tactics. Require Import Types.Forall Types.Prod. Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans