fact: Definition opyon_equiv_0gpd {A : Type} `{HasEquivs A} {a b : A} (f : opyon1_0gpd a $<~> opyon1_0gpd b) : b $<~> a.
imports: Basics.Overture Basics.Tactics WildCat.Core WildCat.Equiv WildCat.Universe WildCat.Opposite WildCat.FunctorCat WildCat.NatTrans WildCat.Prod WildCat.ZeroGroupoid