Proposition isMonic_formula_to_partial_setoid_incl_eq {A : ty H} (φ : form A) (X : partial_setoid H) {ψ₁ ψ₂ : partial_setoid_morphism X (formula_to_partial_setoid φ)} (p : partial_setoid_comp_morphism ψ₁ (formula_to_partial_setoid_incl φ) = partial_setoid_comp_morphism ψ₂ (formula_to_partial_setoid_incl φ)) : ψ₁ ⊢ ψ₂. Proof. refine (hyperdoctrine_cut (@from_eq_partial_setoid_morphism_f _ _ _ _ _ p _ ψ₁ (π₁ (tm_var _)) (π₂ (tm_var _)) _) _). - cbn. simplify_form. use exists_intro. + exact (π₂ (tm_var _)). + simplify. use conj_intro. * rewrite <- hyperdoctrine_pair_eta. rewrite hyperdoctrine_id_subst. apply hyperdoctrine_hyp. * use conj_intro. ** apply hyperdoctrine_refl. ** use hyperdoctrine_cut. *** exact (ψ₁ [ ⟨ π₁ (tm_var _) , π₂ (tm_var _) ⟩ ]). *** rewrite <- (hyperdoctrine_pair_eta (tm_var _)). rewrite hyperdoctrine_id_subst. apply hyperdoctrine_hyp. *** refine (hyperdoctrine_cut (partial_setoid_mor_cod_defined ψ₁ (π₁ (tm_var _)) (π₂ (tm_var _)) (hyperdoctrine_hyp _)) _). exact (prop_from_formula_to_partial_setoid φ (hyperdoctrine_hyp _)). - cbn. simplify_form. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. simplify. use hyp_rtrans. use weaken_left. pose (x := π₁ (π₁ (tm_var ((X ×h A) ×h A)))). pose (a := π₂ (tm_var ((X ×h A) ×h A))). pose (a' := π₂ (π₁ (tm_var ((X ×h A) ×h A)))). fold x a a'. rewrite (hyperdoctrine_pair_eta (π₁ (tm_var ((X ×h A) ×h A)))). fold x a'. use hyperdoctrine_eq_transportf. + exact ⟨ x , a ⟩. + use weaken_right. use hyperdoctrine_eq_pair_eq. * apply hyperdoctrine_refl. * 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.PERConstantObjects.