Proposition subobject_to_partial_setoid_mor_laws : @partial_setoid_morphism_laws _ (subobject_to_partial_setoid ψ₁) (subobject_to_partial_setoid ψ₂) ξ. Proof. unfold ξ. repeat split. - do 2 use forall_intro. use impl_intro. use weaken_right. simplify ; cbn. pose (x := π₂ (π₁ (tm_var ((𝟙 ×h X) ×h Y)))). pose (y := π₂ (tm_var ((𝟙 ×h X) ×h Y))). fold x y. use to_subobject_to_partial_setoid_eq. + use weaken_left. use (partial_setoid_mor_dom_defined φ x y). apply hyperdoctrine_hyp. + use weaken_right. use weaken_left. apply hyperdoctrine_hyp. - do 2 use forall_intro. use impl_intro. use weaken_right. simplify ; cbn. pose (x := π₂ (π₁ (tm_var ((𝟙 ×h X) ×h Y)))). pose (y := π₂ (tm_var ((𝟙 ×h X) ×h Y))). fold x y. use to_subobject_to_partial_setoid_eq. + use weaken_left. use (partial_setoid_mor_cod_defined φ x y). apply hyperdoctrine_hyp. + do 2 use weaken_right. apply hyperdoctrine_hyp. - do 4 use forall_intro. use impl_intro. use weaken_right. do 2 use impl_intro. simplify ; cbn. pose (x₁ := π₂ (π₁ (π₁ (π₁ (tm_var ((((𝟙 ×h X) ×h X) ×h Y) ×h Y)))))). pose (x₂ := π₂ (π₁ (π₁ (tm_var ((((𝟙 ×h X) ×h X) ×h Y) ×h Y))))). pose (y₁ := π₂ (π₁ (tm_var ((((𝟙 ×h X) ×h X) ×h Y) ×h Y)))). pose (y₂ := π₂ (tm_var ((((𝟙 ×h X) ×h X) ×h Y) ×h Y))). fold x₁ x₂ y₁ y₂. repeat use conj_intro. + use (partial_setoid_mor_eq_defined φ). * exact x₁. * exact y₁. * do 2 use weaken_left. use (from_subobject_to_partial_setoid_eq ψ₁). apply hyperdoctrine_hyp. * use weaken_left. use weaken_right. use (from_subobject_to_partial_setoid_eq ψ₂). apply hyperdoctrine_hyp. * use weaken_right. use weaken_left. apply hyperdoctrine_hyp. + use per_subobject_eq. * exact x₁. * do 2 use weaken_left. use (from_subobject_to_partial_setoid_eq ψ₁). apply hyperdoctrine_hyp. * do 2 use weaken_right. use weaken_left. apply hyperdoctrine_hyp. + use per_subobject_eq. * exact y₁. * use weaken_left. use weaken_right. use (from_subobject_to_partial_setoid_eq ψ₂). apply hyperdoctrine_hyp. * do 3 use weaken_right. apply hyperdoctrine_hyp. - do 3 use forall_intro. use impl_intro. use weaken_right. use impl_intro. simplify ; cbn. pose (x := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h X) ×h Y) ×h Y))))). pose (y₁ := π₂ (π₁ (tm_var (((𝟙 ×h X) ×h Y) ×h Y)))). pose (y₂ := π₂ (tm_var (((𝟙 ×h X) ×h Y) ×h Y))). fold x y₁ y₂. use to_subobject_to_partial_setoid_eq. + use (partial_setoid_mor_unique_im φ). * exact x. * do 2 use weaken_left. apply hyperdoctrine_hyp. * use weaken_right. use weaken_left. apply hyperdoctrine_hyp. + use weaken_left. do 2 use weaken_right. apply hyperdoctrine_hyp. - use forall_intro ; cbn. use impl_intro. use weaken_right. refine (exists_elim (partial_setoid_mor_hom_exists φ _) _). + use (from_subobject_to_partial_setoid_eq ψ₁). apply hyperdoctrine_hyp. + simplify_form. 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 exists_intro. { exact y. } simplify ; cbn. fold x y. repeat use conj_intro. * use weaken_right. apply hyperdoctrine_hyp. * use weaken_left. use from_subobject_to_partial_setoid_sub. ** exact x. ** apply hyperdoctrine_hyp. * use (per_subobject_mor p). ** exact x. ** use weaken_right. apply hyperdoctrine_hyp. ** use weaken_left. use (from_subobject_to_partial_setoid_sub ψ₁). *** exact x. *** 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.