Definition comp_preserves_exponentials : preserves_exponentials E₁ E₃ (composition_preserves_binproduct HF HG). Proof. intros x y. use is_z_isomorphism_path. - exact (#G(preserves_exponentials_map E₁ E₂ HF x y) · preserves_exponentials_map E₂ E₃ HG (F x) (F y)). - apply comp_preserves_exponentials_eq. - use is_z_isomorphism_comp. + use functor_on_is_z_isomorphism. apply HFE. + apply HGE. Defined.
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.