fact: Record Fun01 (A B : Type) `{IsGraph A} `{IsGraph B} := { fun01_F : A -> B; fun01_is0functor : Is0Functor fun01_F; }.
imports: Basics.Overture Basics.Tactics WildCat.Core WildCat.Equiv WildCat.Induced WildCat.NatTrans