Lemma subobject_classifier_partial_setoid_map_unique_lem : (χ ∧ Prf [π₂ (tm_var (Y ×h Ω))] ⊢ ∃h (φ [⟨ π₂ (tm_var ((Y ×h Ω) ×h X)) , π₁ (π₁ (tm_var ((Y ×h Ω) ×h X))) ⟩])). Proof. pose (y := π₁ (tm_var (Y ×h Ω))). pose (ω := π₂ (tm_var (Y ×h Ω))). fold y ω. assert (χ ∧ Prf [ω] ⊢ y ~ y) as q₁. { use weaken_left. rewrite <- (hyperdoctrine_id_subst χ). rewrite (hyperdoctrine_pair_eta (tm_var (Y ×h omega_partial_setoid))). cbn. fold y ω. exact (partial_setoid_mor_dom_defined χ y ω (hyperdoctrine_hyp _)). } pose (fy := point_partial_setoid_morphism H (χ ∧ Prf [ω]) y q₁). assert (partial_setoid_comp_morphism fy χ = partial_setoid_comp_morphism (partial_setoid_morphism_to_terminal _) omega_partial_setoid_true) as feq. { use eq_partial_setoid_morphism ; cbn. - use (exists_elim (hyperdoctrine_hyp _)). rewrite conj_subst. use weaken_right. rewrite exists_subst. use exists_intro ; [ apply !! | ]. unfold y, ω. simplify_form. rewrite !partial_setoid_subst. simplify. rewrite (hyperdoctrine_pair_eta (π₁ (π₁ (tm_var (((Y ×h Ω) ×h Ω) ×h Y))))). clear y ω q₁ fy. pose (y₁ := π₁ (π₁ (π₁ (tm_var (((Y ×h Ω) ×h Ω) ×h Y))))). pose (ω₁ := π₂ (π₁ (π₁ (tm_var (((Y ×h Ω) ×h Ω) ×h Y))))). pose (ω₂ := π₂ (π₁ (tm_var (((Y ×h Ω) ×h Ω) ×h Y)))). pose (y₂ := π₂ (tm_var (((Y ×h Ω) ×h Ω) ×h Y))). fold y₁ y₂ ω₁ ω₂. simplify. use conj_intro. + unfold partial_setoid_formula. cbn. simplify. repeat use conj_intro. * apply hyperdoctrine_refl. * do 3 use weaken_left. apply hyperdoctrine_hyp. * do 2 use weaken_left. use weaken_right. apply hyperdoctrine_hyp. + use from_eq_in_omega_partial_setoid_left. * exact ω₁. * use (partial_setoid_mor_unique_im χ). ** exact y₁. ** do 3 use weaken_left. apply hyperdoctrine_hyp. ** use partial_setoid_mor_eq_defined. *** exact y₂. *** exact ω₂. *** use weaken_left. use weaken_right. apply hyperdoctrine_hyp. *** use weaken_right. exact (partial_setoid_mor_cod_defined χ _ _ (hyperdoctrine_hyp _)). *** use weaken_right. apply hyperdoctrine_hyp. * do 2 use weaken_left. use weaken_right. apply hyperdoctrine_hyp. - use (exists_elim (hyperdoctrine_hyp _)). rewrite conj_subst. use weaken_right. rewrite exists_subst. use exists_intro. { exact (π₁ (π₁ (π₁ (tm_var _)))). } unfold y, ω. simplify_form. rewrite !partial_setoid_subst. simplify. rewrite (hyperdoctrine_pair_eta (π₁ (π₁ (tm_var (((Y ×h Ω) ×h Ω) ×h 𝟙))))). clear y ω q₁ fy. pose (y := π₁ (π₁ (π₁ (tm_var (((Y ×h Ω) ×h Ω) ×h 𝟙))))). pose (ω₁ := π₂ (π₁ (π₁ (tm_var (((Y ×h Ω) ×h Ω) ×h 𝟙))))). pose (ω₂ := π₂ (π₁ (tm_var (((Y ×h Ω) ×h Ω) ×h 𝟙)))). pose (t := π₂ (tm_var (((Y ×h Ω) ×h Ω) ×h 𝟙))). fold y t ω₁ ω₂. unfold partial_setoid_formula. cbn. simplify. use hyp_ltrans. use weaken_right. repeat use conj_intro. + do 2 use weaken_left. apply hyperdoctrine_hyp. + use weaken_left. use weaken_right. apply hyperdoctrine_hyp. + do 2 use weaken_left. exact (partial_setoid_mor_dom_defined χ _ _ (hyperdoctrine_hyp _)). + use (partial_setoid_mor_eq_defined χ). * exact y. * exact ω₁. * do 2 use weaken_left. exact (partial_setoid_mor_dom_defined χ _ _ (hyperdoctrine_hyp _)). * use eq_in_omega_partial_setoid. use iff_true_true. ** use weaken_left. use weaken_right. apply hyperdoctrine_hyp. ** use weaken_right. apply hyperdoctrine_hyp. * do 2 use weaken_left. apply hyperdoctrine_hyp. } pose (PullbackArrow (make_Pullback _ Hχ) (formula_to_partial_setoid H (χ ∧ Prf [ω])) fy (partial_setoid_morphism_to_terminal _) feq) as g. cbn in g. refine (weaken_cut _ _). { simple refine (partial_setoid_mor_hom_exists g _). cbn. apply tm_var. unfold partial_setoid_formula. cbn. simplify. repeat use conj_intro. + use hyperdoctrine_refl. + use weaken_left. rewrite hyperdoctrine_id_subst. apply hyperdoctrine_hyp. + use weaken_right. apply hyperdoctrine_hyp. } cbn. use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite conj_subst. use hyp_ltrans. use weaken_right. simplify. pose (y' := π₁ (π₁ (tm_var ((Y ×h Ω) ×h X)))). pose (ω' := π₂ (π₁ (tm_var ((Y ×h Ω) ×h X)))). pose (x' := π₂ (tm_var ((Y ×h Ω) ×h X))). rewrite (hyperdoctrine_pair_eta (π₁ (tm_var ((Y ×h Ω) ×h X)))). unfold y, ω. fold x' ω' y'. simplify. pose (@from_eq_partial_setoid_morphism_b _ _ _ _ _ (PullbackArrow_PullbackPr1 (make_Pullback _ Hχ) _ _ _ feq) _ ((χ [⟨ y', ω' ⟩] ∧ Prf [ω']) ∧ g [⟨ ⟨ y', ω' ⟩, x' ⟩]) (π₁ (tm_var _)) (π₁ (π₁ (tm_var _)))). cbn in h. refine (hyperdoctrine_cut (h _) _). { unfold y, ω. simplify_form. rewrite partial_setoid_subst. simplify. rewrite (hyperdoctrine_pair_eta (π₁ (tm_var ((Y ×h Ω) ×h X)))). fold x' y' ω'. simplify. repeat use conj_intro. + do 2 use weaken_left. apply hyperdoctrine_hyp. + use weaken_left. use weaken_right. apply hyperdoctrine_hyp. + do 2 use weaken_left. exact (partial_setoid_mor_dom_defined χ _ _ (hyperdoctrine_hyp _)). } rewrite exists_subst. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. simplify. unfold x', y'. simplify. use exists_intro. { exact (π₂ (tm_var _)). } simplify. 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.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.Tripos. Require Import UniMath.CategoryTheory.Hyperdoctrines.GenericPredicate. 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.PERTerminal. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMonomorphisms.