Lemma partial_setoid_mono_eq_lem {H : first_order_hyperdoctrine} {X Y : partial_setoid H} (φ : partial_setoid_morphism X Y) (Hφ : isMonic (C := category_of_partial_setoids H) φ) {Γ : ty H} {Δ : form Γ} {x₁ x₂ : tm Γ X} {y : tm Γ Y} (p₁ : Δ ⊢ φ[⟨ x₁ , y ⟩]) (p₂ : Δ ⊢ φ[⟨ x₂ , y ⟩]) (r₁ : Δ ⊢ x₁ ~ x₁) (r₂ : Δ ⊢ x₂ ~ x₂) (fx₁ := point_partial_setoid_morphism H Δ x₁ r₁) (fx₂ := point_partial_setoid_morphism H Δ x₂ r₂) : partial_setoid_comp_morphism fx₁ φ ⊢ partial_setoid_comp_morphism fx₂ φ. Proof. assert (r₃ : Δ ⊢ y ~ y). { refine (hyperdoctrine_cut p₂ _). exact (partial_setoid_mor_cod_defined φ _ _ (hyperdoctrine_hyp _)). } cbn. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. rewrite exists_subst. pose (a := π₂ (tm_var ((Γ ×h Y) ×h X))). pose (b := π₂ (π₁ (tm_var ((Γ ×h Y) ×h X)))). pose (c := π₁ (π₁ (tm_var ((Γ ×h Y) ×h X)))). use exists_intro. { exact (x₂ [ c ]tm). } simplify_form. rewrite !partial_setoid_subst. simplify. fold a b c. repeat use conj_intro. - do 2 use weaken_left. apply hyperdoctrine_hyp. - do 2 use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst c r₂) _). rewrite partial_setoid_subst. apply hyperdoctrine_hyp. - use (partial_setoid_mor_eq_defined φ). + exact (x₂ [ c ]tm). + exact (y [ c ]tm). + do 2 use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst c r₂) _). rewrite partial_setoid_subst. apply hyperdoctrine_hyp. + use (partial_setoid_mor_unique_im φ). * exact a. * use (partial_setoid_mor_eq_defined φ). ** exact (x₁ [ c ]tm). ** exact (y [ c ]tm). ** use weaken_left. use weaken_right. use partial_setoid_sym. apply hyperdoctrine_hyp. ** do 2 use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst c r₃) _). rewrite partial_setoid_subst. apply hyperdoctrine_hyp. ** do 2 use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst c p₁) _). simplify. apply hyperdoctrine_hyp. * use weaken_right. apply hyperdoctrine_hyp. + do 2 use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst c p₂) _). simplify. 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.PERConstantObjects.