proposition: Lemma triangle_helper2 x y g : (equiv_adjunction adj x y)^-1 g = adjunction_unit y $o fmap F g.
proof: Proof. epose (n1 := is1natural_natequiv (natequiv_inverse (natequiv_adjunction_l _)) _ _ _ _). clearbody n1; cbv in n1. refine (_ @ n1). by rewrite cat_idl_strong. 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