Proposition per_subobject_exists_laws : per_subobject_laws per_subobject_exists_form. Proof. split. - use forall_intro. use impl_intro. use weaken_right. unfold per_subobject_exists_form. simplify. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. rewrite partial_setoid_subst. simplify. pose (a := π₂ (tm_var ((𝟙 ×h B) ×h A))). pose (b := π₂ (π₁ (tm_var ((𝟙 ×h B) ×h A)))). fold a b. use weaken_left. use (partial_setoid_mor_cod_defined φ a b). apply hyperdoctrine_hyp. - do 2 use forall_intro. use impl_intro. use weaken_right. use impl_intro. use hyp_sym. unfold per_subobject_exists_form. simplify. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite conj_subst. use hyp_ltrans. use weaken_right. rewrite partial_setoid_subst. simplify. pose (b₁ := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h B) ×h B) ×h A))))). pose (b₂ := π₂ (π₁ (tm_var (((𝟙 ×h B) ×h B) ×h A)))). pose (a := π₂ (tm_var (((𝟙 ×h B) ×h B) ×h A))). fold b₁ b₂ a. use exists_intro. + exact a. + simplify. fold a b₁ b₂. use conj_intro. * use (partial_setoid_mor_eq_defined φ). ** exact a. ** exact b₁. ** use weaken_right. use weaken_left. use (partial_setoid_mor_dom_defined φ a b₁). apply hyperdoctrine_hyp. ** use weaken_left. apply hyperdoctrine_hyp. ** use weaken_right. use weaken_left. apply hyperdoctrine_hyp. * do 2 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.DependentSums. Require Import UniMath.CategoryTheory.Limits.Pullbacks. 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.PERTerminal. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMonomorphisms. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERConstantObjects. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.SubobjectDispCat.