fact: Definition adjunction_triangle2 : Transformation (nattrans_comp (nattrans_postwhisker G adjunction_unit) (nattrans_prewhisker adjunction_counit G)) (nattrans_id _).
imports: Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences WildCat.Core WildCat.NatTrans WildCat.Equiv WildCat.Prod WildCat.Opposite WildCat.Yoneda WildCat.FunctorCat WildCat.Universe Types.Prod