Definition distributivity_fiberwise_exponentials {C : category} {D : disp_cat C} {HD : cleaving D} {P : fiberwise_binproducts HD} (CP : fiberwise_bincoproducts HD) (E : fiberwise_exponentials P) {x : C} (xx yy zz : D[{x}]) : z_iso (preserves_bincoproduct_to_bincoproduct (constprod_functor1 (pr1 P x) xx) (preserves_bincoproduct_constprod_fib E xx) (bincoprod_in_fib CP yy zz)) (bincoprod_in_fib CP (BinProductObject _ (binprod_in_fib P xx yy)) (BinProductObject _ (binprod_in_fib P xx zz))). Proof. exact (preserves_bincoproduct_to_z_iso _ (preserves_bincoproduct_constprod_fib E xx) (bincoprod_in_fib CP yy zz) (bincoprod_in_fib CP (BinProductObject _ (binprod_in_fib P xx yy)) (BinProductObject _ (binprod_in_fib P xx zz)))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproducts. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.exponentials.