Definition make_fiberwise_binproducts_locally_propositional : fiberwise_binproducts HD. Proof. split. - exact make_binproduct_fiber_locally_propositional. - intros Γ₁ Γ₂ s. use preserves_binproduct_if_preserves_chosen. + apply make_binproduct_fiber_locally_propositional. + abstract (intros φ ψ ; use (isBinProduct_z_iso (isBinProduct_BinProduct _ (make_binproduct_fiber_locally_propositional Γ₁ (fiber_functor_from_cleaving D HD s φ) (fiber_functor_from_cleaving D HD s ψ)))) ; [ | apply HD' | apply HD' ] ; use make_z_iso ; [ | apply and_sub | split ; apply HD' ] ; apply BinProductArrow ; [ exact (#(fiber_functor_from_cleaving D HD s) (BinProductPr1 _ _)) | exact (#(fiber_functor_from_cleaving D HD s) (BinProductPr2 _ _)) ]). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. 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.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Preservation.