proposition: Proposition exp_eta {x y z : C} (f : z --> exp x y) : f = exp_lam (BinProductOfArrows C _ _ (identity x) f · exp_eval x y).
proof: Proof. unfold exp_lam. rewrite functor_comp. rewrite !assoc. refine (!_). etrans. { apply maponpaths_2. exact (!(nat_trans_ax (unit_from_are_adjoints (pr2 (expC x))) _ _ f)). } refine (_ @ id_right _). rewrite !assoc'. apply maponpaths. exact (triangle_id_right_ad (pr2 (expC x)) _). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.catiso UniMath.CategoryTheory.CategoryEquality UniMath.CategoryTheory.Core.Univalence