proposition: Proposition exp_lam_natural {w x y z : C} (f : prodC y x --> z) (s : w --> x) : s · exp_lam f = exp_lam (BinProductOfArrows _ _ _ (identity _ ) s · f).
proof: Proof. use exp_funext. intros a h. etrans. { do 2 apply maponpaths_2. exact (!(id_right _)). } rewrite <- BinProductOfArrows_comp. rewrite !assoc'. rewrite exp_beta. refine (!_). etrans. { do 2 apply maponpaths_2. exact (!(id_right _)). } etrans. { apply maponpaths_2. apply maponpaths. exact (!(id_left _)). } rewrite <- BinProductOfArrows_comp. rewrite !assoc'. rewrite exp_beta. rewrite !assoc. apply maponpaths_2. rewrite BinProductOfArrows_comp. rewrite id_left, id_right. apply idpath. 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