proposition: Lemma triangle_helper1 x y f : equiv_adjunction adj x y f = fmap G f $o adjunction_counit x.
proof: Proof. refine (_ @ is1natural_equiv_adjunction_r adj _ _ _ _ _). by cbv; rewrite (cat_idr_strong f). Qed.
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