Proposition subobject_classifier_partial_setoid_map_unique : χ = subobject_classifier_partial_setoid_map. Proof. use eq_partial_setoid_morphism ; cbn. - pose (y := π₁ (tm_var (Y ×h Ω))). pose (ω := π₂ (tm_var (Y ×h Ω))). fold y ω. use conj_intro. + use (partial_setoid_mor_dom_defined χ y ω). unfold y, ω. rewrite <- hyperdoctrine_pair_eta. simplify. apply hyperdoctrine_hyp. + use iff_intro. * use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite conj_subst. use hyp_ltrans. use weaken_right. simplify_form. unfold y, ω ; clear y ω. simplify. pose (y := π₁ (π₁ (tm_var ((Y ×h Ω) ×h X)))). pose (ω := π₂ (π₁ (tm_var ((Y ×h Ω) ×h X)))). pose (x := π₂ (tm_var ((Y ×h Ω) ×h X))). fold y ω x. rewrite (hyperdoctrine_pair_eta (π₁ (tm_var _))). fold y ω. pose (from_eq_partial_setoid_morphism_f p (t₁ := x) (t₂ := ω) (Δ := χ [⟨ y, ω ⟩] ∧ φ [⟨ x, y ⟩])) as r. cbn in r. rewrite !exists_subst in r. use (exists_elim (r _)) ; clear r. ** use exists_intro. { exact y. } simplify. use hyp_sym. apply hyperdoctrine_hyp. ** unfold y, ω, x ; clear x y ω. simplify_form. rewrite partial_setoid_subst. simplify. pose (y := π₁ (π₁ (π₁ (tm_var (((Y ×h Ω) ×h X) ×h 𝟙))))). pose (ω := π₂ (π₁ (π₁ (tm_var (((Y ×h Ω) ×h X) ×h 𝟙))))). pose (x := π₂ (π₁ (tm_var (((Y ×h Ω) ×h X) ×h 𝟙)))). fold x y ω. do 2 use weaken_right. apply hyperdoctrine_hyp. * unfold ω, y. simplify. apply subobject_classifier_partial_setoid_map_unique_lem. - use (exists_elim (partial_setoid_mor_hom_exists χ (weaken_left (hyperdoctrine_hyp _) _))). simplify_form. rewrite partial_setoid_subst. simplify. pose (y := π₁ (π₁ (tm_var ((Y ×h Ω) ×h Ω)))). pose (ω₁ := π₂ (π₁ (tm_var ((Y ×h Ω) ×h Ω)))). pose (ω₂ := π₂ (tm_var ((Y ×h Ω) ×h Ω))). cbn. fold y ω₁ ω₂. rewrite (hyperdoctrine_pair_eta (π₁ (tm_var ((Y ×h Ω) ×h Ω)))). fold y ω₁. use (partial_setoid_mor_eq_defined χ). + exact y. + exact ω₂. + do 2 use weaken_left. apply hyperdoctrine_hyp. + use partial_setoid_sym. use eq_in_omega_partial_setoid. use iff_intro. * pose (((y ~ y ∧ (∃h (φ [⟨ π₂ (tm_var _) , π₁ (π₁ (π₁ (tm_var _))) ⟩]) ⇔ Prf [ ω₁ ])) ∧ χ [⟨ y, ω₂ ⟩]) ∧ Prf [ ω₁ ]) as Δ. pose (y ~ y ∧ χ [⟨ y, ω₂ ⟩] ∧ (∃h (φ [⟨ π₂ (tm_var _) , π₁ (π₁ (π₁ (tm_var _))) ⟩]))) as Δ'. assert (Δ ⊢ Δ') as r. { unfold Δ, Δ'. repeat use conj_intro. ** do 3 use weaken_left. apply hyperdoctrine_hyp. ** use weaken_left. use weaken_right. apply hyperdoctrine_hyp. ** use iff_elim_right. *** exact (Prf [ ω₁ ]). *** do 2 use weaken_left. use weaken_right. apply hyperdoctrine_hyp. *** use weaken_right. apply hyperdoctrine_hyp. } refine (hyperdoctrine_cut r _). unfold Δ'. use hyp_rtrans. use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite conj_subst. use hyp_ltrans. use weaken_right. unfold y, ω₁, ω₂, Δ, Δ' ; clear r Δ Δ' y ω₁ ω₂. simplify_form. rewrite partial_setoid_subst. simplify. pose (y := π₁ (π₁ (π₁ (tm_var (((Y ×h Ω) ×h Ω) ×h X))))). pose (ω₁ := π₂ (π₁ (π₁ (tm_var (((Y ×h Ω) ×h Ω) ×h X))))). pose (ω₂ := π₂ (π₁ (tm_var (((Y ×h Ω) ×h Ω) ×h X)))). pose (x := π₂ (tm_var (((Y ×h Ω) ×h Ω) ×h X))). cbn. fold y ω₁ ω₂ x. pose (from_eq_partial_setoid_morphism_f p (t₁ := x) (t₂ := ω₂) (Δ := (y ~ y ∧ χ [⟨ y, ω₂ ⟩]) ∧ φ [⟨ x, y ⟩])) as r. cbn in r. rewrite !exists_subst in r. use (exists_elim (r _)). ** use exists_intro. { exact y. } simplify. use hyp_ltrans. use weaken_right. use hyp_sym. apply hyperdoctrine_hyp. ** simplify_form. rewrite !partial_setoid_subst. simplify. do 2 use weaken_right. apply hyperdoctrine_hyp. * refine (iff_elim_left _ _). { do 2 use weaken_left. use weaken_right. apply hyperdoctrine_hyp. } do 2 use hyp_ltrans. do 2 use weaken_right. pose (hyperdoctrine_proof_subst ⟨ y , ω₂ ⟩ subobject_classifier_partial_setoid_map_unique_lem) as q. refine (hyperdoctrine_cut _ (hyperdoctrine_cut q _)). ** simplify. apply hyperdoctrine_hyp. ** unfold y. simplify. 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.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.