Proposition isMonic_subobject_to_partial_setoid_incl : isMonic (C := category_of_partial_setoids H) subobject_to_partial_setoid_incl. Proof. intros W ψ₁ ψ₂ p. cbn in W, ψ₁, ψ₂, p. use eq_partial_setoid_morphism. - rewrite <- (hyperdoctrine_id_subst ψ₁). rewrite <- (hyperdoctrine_id_subst ψ₂). rewrite (hyperdoctrine_pair_eta (tm_var _)). cbn. pose (w := π₁ (tm_var (W ×h X))). pose (x := π₂ (tm_var (W ×h X))). fold w x. refine (hyperdoctrine_cut _ _). { apply (from_eq_partial_setoid_morphism_f p (Δ := ψ₁ [⟨ w , x ⟩]) (t₁ := w) (t₂ := x)). cbn. simplify_form. use exists_intro. { exact x. } simplify. use conj_intro. + apply hyperdoctrine_hyp. + use (partial_setoid_mor_cod_defined ψ₁ w x). apply hyperdoctrine_hyp. } cbn. unfold w, x ; clear w x. simplify_form. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. simplify. pose (w := π₁ (π₁ (tm_var ((W ×h X) ×h X)))). pose (x₁ := π₂ (π₁ (tm_var ((W ×h X) ×h X)))). pose (x₂ := π₂ (tm_var ((W ×h X) ×h X))). fold w x₁ x₂. use (partial_setoid_mor_eq_defined ψ₂). + exact w. + exact x₂. + use weaken_left. use (partial_setoid_mor_dom_defined ψ₂ w x₂). apply hyperdoctrine_hyp. + use weaken_right. apply hyperdoctrine_hyp. + use weaken_left. apply hyperdoctrine_hyp. - rewrite <- (hyperdoctrine_id_subst ψ₁). rewrite <- (hyperdoctrine_id_subst ψ₂). rewrite (hyperdoctrine_pair_eta (tm_var _)). cbn. pose (w := π₁ (tm_var (W ×h X))). pose (x := π₂ (tm_var (W ×h X))). fold w x. refine (hyperdoctrine_cut _ _). { apply (from_eq_partial_setoid_morphism_b p (Δ := ψ₂ [⟨ w , x ⟩]) (t₁ := w) (t₂ := x)). cbn. simplify_form. use exists_intro. { exact x. } simplify. use conj_intro. + apply hyperdoctrine_hyp. + use (partial_setoid_mor_cod_defined ψ₂ w x). apply hyperdoctrine_hyp. } cbn. unfold w, x ; clear w x. simplify_form. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. simplify. pose (w := π₁ (π₁ (tm_var ((W ×h X) ×h X)))). pose (x₁ := π₂ (π₁ (tm_var ((W ×h X) ×h X)))). pose (x₂ := π₂ (tm_var ((W ×h X) ×h X))). fold w x₁ x₂. use (partial_setoid_mor_eq_defined ψ₁). + exact w. + exact x₂. + use weaken_left. use (partial_setoid_mor_dom_defined ψ₁ w x₂). apply hyperdoctrine_hyp. + use weaken_right. apply hyperdoctrine_hyp. + use weaken_left. 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.