Definition fiberwise_bincoproducts_per_subobject : fiberwise_bincoproducts (disp_cat_per_subobject_cleaving H). Proof. use make_fiberwise_bincoproducts_locally_propositional. - apply locally_prop_disp_cat_per_subobject. - intros Γ ψ₁ ψ₂. exact (per_subobject_disj ψ₁ ψ₂). - intros Γ ψ₁ ψ₂. exact (per_subobject_disj_intro_left ψ₁ ψ₂). - intros Γ ψ₁ ψ₂. exact (per_subobject_disj_intro_right ψ₁ ψ₂). - intros Γ ψ₁ ψ₂ χ p q. exact (per_subobject_disj_elim ψ₁ ψ₂ p q). - intros Γ₁ Γ₂ s ψ₁ ψ₂. exact (per_subobject_disj_subst s ψ₁ ψ₂). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproducts. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERs. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMorphisms. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERCategory. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.SubobjectDispCat.