make nattrans_flip more natural

Signed-off-by: Ali Caglayan <[email protected]>

Author: Alizter

theories/WildCat/Bifunctor.v

@@ -401,9 +401,9 @@ Defined.
 Definition nattrans_flip {A B C : Type}
   `{Is1Cat A, Is1Cat B, Is1Cat C}
   {F : A -> B -> C} `{!Is0Bifunctor F, !Is1Bifunctor F}
-  {G : B -> A -> C} `{!Is0Bifunctor G, !Is1Bifunctor G}
-  : NatTrans (uncurry F) (uncurry (flip G))
-    -> NatTrans (uncurry (flip F)) (uncurry G).
+  {G : A -> B -> C} `{!Is0Bifunctor G, !Is1Bifunctor G}
+  : NatTrans (uncurry F) (uncurry G)
+    -> NatTrans (uncurry (flip F)) (uncurry (flip G)).
 Proof.
   intros [alpha nat].
   snrapply Build_NatTrans.
@@ -412,14 +412,6 @@ Proof.
     exact (nat (a, b) (a', b') (f, g)).
 Defined.
 
-Definition nattrans_flip' {A B C : Type}
-  `{Is1Cat A, Is1Cat B, Is1Cat C}
-  {F : A -> B -> C} `{!Is0Bifunctor F, !Is1Bifunctor F}
-  {G : B -> A -> C} `{!Is0Bifunctor G, !Is1Bifunctor G}
-  : NatTrans (uncurry (flip F)) (uncurry G)
-    -> NatTrans (uncurry F) (uncurry (flip G))
-  := nattrans_flip (F:=flip F) (G:=flip G).
-
 (** ** Opposite Bifunctors *)
 
 (** There are a few more combinations we can do for this, such as profunctors, but we will leave those for later. *)