Proposition monic_to_per_subobject_laws : per_subobject_laws ζ. Proof. unfold ζ. split. - use forall_intro. use impl_intro. use weaken_right. simplify. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. rewrite partial_setoid_subst. simplify. pose (x := π₂ (π₁ (tm_var ((𝟙 ×h X) ×h Y)))). pose (y := π₂ (tm_var ((𝟙 ×h X) ×h Y))). fold x y. use (partial_setoid_mor_cod_defined φ y x). apply hyperdoctrine_hyp. - do 2 use forall_intro. use impl_intro. use weaken_right. use impl_intro. use hyp_sym. simplify. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite conj_subst. use hyp_ltrans. use weaken_right. simplify_form. rewrite partial_setoid_subst. simplify. pose (x₁ := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h X) ×h X) ×h Y))))). pose (x₂ := π₂ (π₁ (tm_var (((𝟙 ×h X) ×h X) ×h Y)))). pose (y := π₂ (tm_var (((𝟙 ×h X) ×h X) ×h Y))). fold x₁ x₂ y. use exists_intro. { exact y. } simplify. fold x₂. use partial_setoid_mor_eq_defined. + exact y. + exact x₁. + use weaken_right. use (partial_setoid_mor_dom_defined φ y x₁). apply hyperdoctrine_hyp. + 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.Monics. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.MonoCodomain. Require Import UniMath.CategoryTheory.DisplayedCats.MonoCodomain.FiberMonoCod. 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.PERMonomorphisms. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.SubobjectDispCat.