fact: Definition fun01_hom {A} `{Is01Cat A} : Fun01 (A^op * A) Type := @Build_Fun01 _ _ _ _ _ is0functor_hom.
imports: Basics.Overture Basics.Tactics WildCat.Core WildCat.Equiv WildCat.Universe WildCat.Opposite WildCat.FunctorCat WildCat.NatTrans WildCat.Prod WildCat.ZeroGroupoid