(A B : Type) `{IsGraph A} `{IsGraph B} := { fun01_F : A -> B; fun01_is0functor : Is0Functor fun01_F; }.
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.