Proposition comp_preserves_exponentials_eq (x y : C₁) : # G (preserves_exponentials_map E₁ E₂ HF x y) · preserves_exponentials_map E₂ E₃ HG (F x) (F y) = preserves_exponentials_map E₁ E₃ (composition_preserves_binproduct HF HG) x y. Proof. unfold preserves_exponentials_map ; cbn. refine (exp_eta _ _ @ _). apply maponpaths. etrans. { rewrite <- BinProductOfArrows_idxcomp. rewrite !assoc'. rewrite exp_beta. rewrite !assoc. rewrite <- (functor_id G). apply maponpaths_2. refine (!_). apply preserves_binproduct_of_arrows. } rewrite !assoc'. etrans. { apply maponpaths. refine (!(functor_comp G _ _) @ _). apply maponpaths. apply exp_beta. } rewrite functor_comp. rewrite !assoc. apply maponpaths_2. use z_iso_inv_on_right. etrans. { apply (preserves_binproduct_to_preserves_arrow G HG (preserves_binproduct_to_binproduct F HF (BC₁ x (exp (E₁ x) y))) (BC₃ _ _)). } cbn. 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.