{A} {B} `{Is01Cat B} (F : A -> B) (G : A -> B) (alpha : F $=> G) : Transformation (A:=A^op) (B:=fun _ => B^op) G (F : A^op -> B^op) := alpha.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.