Definition make_bincoproduct_fiber_locally_propositional (Γ : C) : BinCoproducts D[{Γ}]. Proof. intros φ ψ. use make_BinCoproduct. - exact (or Γ φ ψ). - exact (or_in1 Γ φ ψ). - exact (or_in2 Γ φ ψ). - intros χ p₁ p₂. use iscontraprop1. + abstract (use invproofirrelevance ; intros q₁ q₂ ; use subtypePath ; [ intro ; apply isapropdirprod ; apply homset_property | ] ; apply HD'). + simple refine (_ ,, _ ,, _) ; [ | apply HD' | apply HD' ]. exact (or_out Γ φ ψ χ p₁ p₂). 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.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation.