Lemma exponentials_independent_beta {x y z : C} (f : BC₂ x z --> y) : f = BinProductOfArrows C (BC₂ x (exp (E x) y)) (BC₂ x z) (identity x) (exp_lam (E x) (BinProductArrow C (BC₂ x z) (BinProductPr1 C (BC₁ x z)) (BinProductPr2 C (BC₁ x z)) · f)) · (BinProductArrow C (BC₁ x (exp (E x) y)) (BinProductPr1 C (BC₂ x (exp (E x) y))) (BinProductPr2 C (BC₂ x (exp (E x) y))) · exp_eval (E x) y). Proof. use (cancel_z_iso' (z_iso_inv (iso_between_BinProduct (BC₂ x z) (BC₁ x z)))). refine (!(exp_beta (E x) _) @ _). rewrite !assoc. apply maponpaths_2. cbn. refine (!_). unfold BinProductOfArrows. rewrite !precompWithBinProductArrow. rewrite !id_right. etrans. { apply maponpaths_2. etrans. { apply BinProductPr1Commutes. } apply BinProductPr1Commutes. } apply maponpaths. rewrite BinProductPr2Commutes. rewrite !assoc. rewrite BinProductPr2Commutes. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.CategoryEquality. Require Import UniMath.CategoryTheory.Core.Univalence.