(A B : Type) `{IsGraph A} `{IsGraph B} : Fun01 A B -> Fun01 A^op B^op. Proof. intros F. rapply (Build_Fun01 A^op B^op F). Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Opposite. Require Import WildCat.Equiv. Require Import WildCat.Induced. Require Import WildCat.NatTrans.