Proposition per_subobject_subst_laws : per_subobject_laws ζ. Proof. split. - unfold ζ. use forall_intro. use impl_intro. use weaken_right. rewrite exists_subst. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. rewrite partial_setoid_subst. simplify. pose (x := π₂ (tm_var ((𝟙 ×h Y) ×h X))). pose (y := π₂ (π₁ (tm_var ((𝟙 ×h Y) ×h X)))). fold x y. use weaken_left. use (partial_setoid_mor_dom_defined φ). + exact x. + apply hyperdoctrine_hyp. - unfold ζ. do 2 use forall_intro. use impl_intro. use weaken_right. use impl_intro. use hyp_sym. rewrite !exists_subst. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite !conj_subst. use hyp_ltrans. use weaken_right. rewrite !partial_setoid_subst. simplify. pose (y₁ := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h Y) ×h Y) ×h X))))). pose (y₂ := π₂ (π₁ (tm_var (((𝟙 ×h Y) ×h Y) ×h X)))). pose (x := π₂ (tm_var (((𝟙 ×h Y) ×h Y) ×h X))). fold y₁ y₂ x. use exists_intro. + exact x. + simplify. fold y₂. use conj_intro. * use (partial_setoid_mor_eq_defined φ). ** exact y₁. ** exact x. ** use weaken_left. apply hyperdoctrine_hyp. ** use weaken_right. use weaken_left. use (partial_setoid_mor_cod_defined φ). *** exact y₁. *** 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.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. 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.