Proposition isaprop_fiberwise_bincoproducts {C : category} {D : disp_univalent_category C} (HD : cleaving D) : isaprop (fiberwise_bincoproducts HD). Proof. use isapropdirprod. - do 3 (use impred ; intro). use isaprop_BinCoproduct. use is_univalent_fiber. apply disp_univalent_category_is_univalent_disp. - do 3 (use impred ; intro). apply isaprop_preserves_bincoproduct. Qed.
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.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation.