Proposition subobject_to_partial_setoid_mor_eq : partial_setoid_comp_morphism subobject_to_partial_setoid_mor (subobject_to_partial_setoid_incl ψ₂) = partial_setoid_comp_morphism (subobject_to_partial_setoid_incl ψ₁) φ. Proof. use eq_partial_setoid_morphism. - use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. cbn ; unfold ξ ; cbn. simplify_form. rewrite !partial_setoid_subst. simplify. pose (x := π₁ (π₁ (tm_var ((X ×h Y) ×h Y)))). pose (y₁ := π₂ (π₁ (tm_var ((X ×h Y) ×h Y)))). pose (y₂ := π₂ (tm_var ((X ×h Y) ×h Y))). fold x y₁ y₂. use exists_intro. { exact x. } simplify_form. rewrite !partial_setoid_subst. simplify. fold x y₁ y₂. repeat use conj_intro. + do 2 use weaken_left. use (partial_setoid_mor_dom_defined φ x y₂). apply hyperdoctrine_hyp. + use weaken_left. use weaken_right. use weaken_left. apply hyperdoctrine_hyp. + use partial_setoid_mor_eq_defined. * exact x. * exact y₂. * do 2 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 weaken_left. apply hyperdoctrine_hyp. - use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. cbn ; unfold ξ ; cbn. simplify_form. rewrite !partial_setoid_subst. simplify. pose (x₁ := π₁ (π₁ (tm_var ((X ×h Y) ×h X)))). pose (y := π₂ (π₁ (tm_var ((X ×h Y) ×h X)))). pose (x₂ := π₂ (tm_var ((X ×h Y) ×h X))). fold x₁ x₂ y. use exists_intro. { exact y. } simplify_form. rewrite !partial_setoid_subst. simplify. fold x₁ x₂ y. repeat use conj_intro. + use partial_setoid_mor_eq_defined. * exact x₂. * exact y. * do 2 use weaken_left. use partial_setoid_sym. apply hyperdoctrine_hyp. * use weaken_right. use (partial_setoid_mor_cod_defined φ x₂ y). apply hyperdoctrine_hyp. * use weaken_right. apply hyperdoctrine_hyp. + use weaken_left. use weaken_right. apply hyperdoctrine_hyp. + use (per_subobject_mor p). * exact x₂. * use weaken_right. apply hyperdoctrine_hyp. * use weaken_left. use per_subobject_eq. ** exact x₁. ** use weaken_left. apply hyperdoctrine_hyp. ** use weaken_right. apply hyperdoctrine_hyp. + use weaken_right. use (partial_setoid_mor_cod_defined φ x₂ y). apply hyperdoctrine_hyp. + use (per_subobject_mor p). * exact x₂. * use weaken_right. apply hyperdoctrine_hyp. * use weaken_left. use per_subobject_eq. ** exact x₁. ** 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.