Lemma exponentials_independent_eta {x y z : C} (f : BC₂ x z --> y) : isaprop (∑ (f' : z --> exp (E x) y), f = # (constprod_functor1 BC₂ x) f' · (iso_between_BinProduct (BC₂ x (exp (E x) y)) (BC₁ x (exp (E x) y)) · exp_eval (E x) y)). Proof. use invproofirrelevance. intros g₁ g₂. pose proof (p := !(pr2 g₁) @ pr2 g₂). cbn in p. unfold BinProduct_of_functors_mor in p. cbn in p. rewrite !assoc in p. rewrite !precompWithBinProductArrow in p. rewrite !(BinProductOfArrowsPr1 _ (BC₂ x (exp (E x) y)) (BC₂ x z)) in p. rewrite !(BinProductOfArrowsPr2 _ (BC₂ x (exp (E x) y)) (BC₂ x z)) in p. rewrite !id_right in p. use subtypePath. { intro. apply homset_property. } refine (exp_eta _ _ @ _ @ !(exp_eta _ _)). apply maponpaths. unfold BinProductOfArrows. rewrite !id_right. simple refine (_ @ maponpaths (λ h, iso_between_BinProduct _ _ · h) p @ _). - cbn. rewrite !assoc. apply maponpaths_2. rewrite precompWithBinProductArrow. rewrite (BinProductPr1Commutes _ _ _ (BC₂ x z)). rewrite !assoc. rewrite (BinProductPr2Commutes _ _ _ (BC₂ x z)). apply idpath. - cbn. rewrite !assoc. apply maponpaths_2. rewrite precompWithBinProductArrow. rewrite (BinProductPr1Commutes _ _ _ (BC₂ x z)). rewrite !assoc. rewrite (BinProductPr2Commutes _ _ _ (BC₂ x z)). 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.