Proposition subobject_to_partial_setoid_incl_laws : @partial_setoid_morphism_laws H subobject_to_partial_setoid X χ. Proof. unfold χ. repeat split. - do 2 use forall_intro. use impl_intro. use weaken_right. cbn. simplify_form. rewrite partial_setoid_subst. simplify. pose (x₁ := π₂ (π₁ (tm_var ((𝟙 ×h X) ×h X)))). pose (x₂ := π₂ (tm_var ((𝟙 ×h X) ×h X))). fold x₁ x₂. use to_subobject_to_partial_setoid_eq. + use weaken_left. exact (partial_setoid_refl_l (hyperdoctrine_hyp _)). + use weaken_right. apply hyperdoctrine_hyp. - do 2 use forall_intro. use impl_intro. use weaken_right. simplify_form. rewrite partial_setoid_subst. simplify. pose (x₁ := π₂ (π₁ (tm_var ((𝟙 ×h X) ×h X)))). pose (x₂ := π₂ (tm_var ((𝟙 ×h X) ×h X))). fold x₁ x₂. use weaken_left. exact (partial_setoid_refl_r (hyperdoctrine_hyp _)). - do 4 use forall_intro ; cbn. use impl_intro. use weaken_right. do 2 use impl_intro. simplify_form. rewrite !partial_setoid_subst. simplify. pose (x₁ := π₂ (π₁ (π₁ (π₁ (tm_var ((((𝟙 ×h X) ×h X) ×h X) ×h X)))))). pose (x₂ := π₂ (π₁ (π₁ (tm_var ((((𝟙 ×h X) ×h X) ×h X) ×h X))))). pose (x₃ := π₂ (π₁ (tm_var ((((𝟙 ×h X) ×h X) ×h X) ×h X)))). pose (x₄ := π₂ (tm_var ((((𝟙 ×h X) ×h X) ×h X) ×h X))). fold x₁ x₂ x₃ x₄. use conj_intro. + use partial_setoid_trans. * exact x₃. * use partial_setoid_trans. ** exact x₁. ** use partial_setoid_sym. do 2 use weaken_left. use from_subobject_to_partial_setoid_eq. apply hyperdoctrine_hyp. ** use weaken_right. use weaken_left. apply hyperdoctrine_hyp. * use weaken_left. use weaken_right. apply hyperdoctrine_hyp. + do 2 use weaken_left. use per_subobject_eq. * exact x₁. * use from_subobject_to_partial_setoid_eq. apply hyperdoctrine_hyp. * use from_subobject_to_partial_setoid_sub. ** exact x₂. ** apply hyperdoctrine_hyp. - do 3 use forall_intro. use impl_intro. use weaken_right. use impl_intro. cbn. simplify_form. rewrite !partial_setoid_subst. simplify. pose (x₁ := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h X) ×h X) ×h X))))). pose (x₂ := π₂ (π₁ (tm_var (((𝟙 ×h X) ×h X) ×h X)))). pose (x₃ := π₂ (tm_var (((𝟙 ×h X) ×h X) ×h X))). fold x₁ x₂ x₃. use partial_setoid_trans. + exact x₁. + use partial_setoid_sym. do 2 use weaken_left. apply hyperdoctrine_hyp. + use weaken_right. use weaken_left. apply hyperdoctrine_hyp. - use forall_intro. use impl_intro. cbn. use weaken_right. pose (x := π₂ (tm_var (𝟙 ×h X))). fold x. use exists_intro. { exact x. } simplify_form. rewrite partial_setoid_subst. simplify. use conj_intro. + use from_subobject_to_partial_setoid_eq. apply hyperdoctrine_hyp. + 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.