Proposition per_subobject_disj_laws : per_subobject_laws (ψ₁ ∨ ψ₂). Proof. split. - use forall_intro. use impl_intro. use weaken_right. simplify. use (disj_elim (hyperdoctrine_hyp _)). + use weaken_right. use (per_subobject_def ψ₁). apply hyperdoctrine_hyp. + use weaken_right. use (per_subobject_def ψ₂). apply hyperdoctrine_hyp. - do 2 use forall_intro. use impl_intro. use weaken_right. use impl_intro. use hyp_sym. simplify. pose (γ₁ := π₂ (π₁ (tm_var ((𝟙 ×h Γ) ×h Γ)))). pose (γ₂ := π₂ (tm_var ((𝟙 ×h Γ) ×h Γ))). fold γ₁ γ₂. use (disj_elim (weaken_left (hyperdoctrine_hyp _) _)). + use hyp_ltrans. use weaken_right. use disj_intro_left. use (per_subobject_eq ψ₁). * exact γ₁. * use weaken_left. apply hyperdoctrine_hyp. * use weaken_right. apply hyperdoctrine_hyp. + use hyp_ltrans. use weaken_right. use disj_intro_right. use (per_subobject_eq ψ₂). * exact γ₁. * use weaken_left. apply hyperdoctrine_hyp. * use weaken_right. apply hyperdoctrine_hyp. Qed.
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.