Proposition is_pullback_subobject_classifier_partial_setoid_map_pr1 : partial_setoid_comp_morphism is_pullback_subobject_classifier_partial_setoid_map φ = ψ₁. Proof. use eq_partial_setoid_morphism ; cbn. - use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. rewrite exists_subst. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite conj_subst. use hyp_ltrans. use weaken_right. simplify. pose (w := π₁ (π₁ (π₁ (tm_var (((W ×h Y) ×h X) ×h Y))))). pose (y₁ := π₂ (π₁ (π₁ (tm_var (((W ×h Y) ×h X) ×h Y))))). pose (x := π₂ (π₁ (tm_var (((W ×h Y) ×h X) ×h Y)))). pose (y₂ := π₂ (tm_var (((W ×h Y) ×h X) ×h Y))). fold w x y₁ y₂. rewrite (hyperdoctrine_pair_eta (π₁ (π₁ (tm_var _)))). fold w y₁. use (partial_setoid_mor_eq_defined ψ₁). + exact w. + exact y₂. + use (partial_setoid_mor_dom_defined ψ₁). * exact y₂. * do 2 use weaken_right. apply hyperdoctrine_hyp. + use (partial_setoid_mor_unique_im φ). * exact x. * use weaken_right. use weaken_left. apply hyperdoctrine_hyp. * use weaken_left. apply hyperdoctrine_hyp. + do 2 use weaken_right. apply hyperdoctrine_hyp. - use (exists_elim (partial_setoid_mor_hom_exists is_pullback_subobject_classifier_partial_setoid_map _)). + exact (π₁ (tm_var _)). + use (partial_setoid_mor_dom_defined ψ₁). * exact (π₂ (tm_var _)). * rewrite <- hyperdoctrine_pair_eta. simplify. apply hyperdoctrine_hyp. + cbn. rewrite exists_subst. use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite conj_subst. use hyp_ltrans. use weaken_right. simplify. pose (w := π₁ (π₁ (π₁ (tm_var (((W ×h Y) ×h X) ×h Y))))). pose (y₁ := π₂ (π₁ (π₁ (tm_var (((W ×h Y) ×h X) ×h Y))))). pose (x := π₂ (π₁ (tm_var (((W ×h Y) ×h X) ×h Y)))). pose (y₂ := π₂ (tm_var (((W ×h Y) ×h X) ×h Y))). fold w x y₁ y₂. use exists_intro. { exact x. } simplify_form. assert (ψ₁ [⟨ w, y₁ ⟩] ∧ φ [⟨ x, y₂ ⟩] ∧ ψ₁ [⟨ w, y₂ ⟩] ⊢ φ [⟨ x, y₁ ⟩]) as r. { use (partial_setoid_mor_eq_defined φ). * exact x. * exact y₂. * use weaken_right. use weaken_left. use (partial_setoid_mor_dom_defined φ x y₂). apply hyperdoctrine_hyp. * use partial_setoid_sym. use (partial_setoid_mor_unique_im ψ₁). ** exact w. ** use weaken_left. apply hyperdoctrine_hyp. ** do 2 use weaken_right. apply hyperdoctrine_hyp. * use weaken_right. use weaken_left. apply hyperdoctrine_hyp. } use conj_intro. * use exists_intro. { exact y₁. } simplify. fold w. rewrite (hyperdoctrine_pair_eta (π₁ (π₁ (tm_var _)))). fold w y₁. use conj_intro. ** exact r. ** use weaken_left. apply hyperdoctrine_hyp. * simplify. fold y₁. rewrite (hyperdoctrine_pair_eta (π₁ (π₁ (tm_var _)))). fold w y₁. exact r. 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.