{A B : Type} `{Is01Cat A} `{Is1Cat B} {F G : A -> B} `{!Is0Functor F, !Is0Functor G} : NatTrans F G -> NatTrans (A:=A^op) (B:=B^op) (G : A^op -> B^op) (F : A^op -> B^op) := fun alpha => Build_NatTrans (trans_op F G alpha) _.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.