Proposition is_pullback_subobject_classifier_partial_setoid_unique : ζ = is_pullback_subobject_classifier_partial_setoid_map. Proof. use eq_partial_setoid_morphism ; cbn. - use (exists_elim (partial_setoid_mor_hom_exists φ _)). + exact (π₂ (tm_var _)). + use (partial_setoid_mor_cod_defined ζ). { exact (π₁ (tm_var _)). } rewrite <- hyperdoctrine_pair_eta. simplify. apply hyperdoctrine_hyp. + rewrite exists_subst. pose (w := π₁ (π₁ (tm_var ((W ×h X) ×h Y)))). pose (x := π₂ (π₁ (tm_var ((W ×h X) ×h Y)))). pose (y := π₂ (tm_var ((W ×h X) ×h Y))). use exists_intro. { exact y. } simplify. fold w x y. rewrite (hyperdoctrine_pair_eta (π₁ (tm_var _))). fold w x. use conj_intro. * use weaken_right. apply hyperdoctrine_hyp. * use (from_eq_partial_setoid_morphism_f ζp) ; cbn. simplify_form. use exists_intro. { exact x. } simplify. apply hyperdoctrine_hyp. - use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. pose (w := π₁ (π₁ (tm_var ((W ×h X) ×h Y)))). pose (x := π₂ (π₁ (tm_var ((W ×h X) ×h Y)))). pose (y := π₂ (tm_var ((W ×h X) ×h Y))). fold w x y. rewrite (hyperdoctrine_pair_eta (π₁ (tm_var _))). fold w x. refine (weaken_cut (from_eq_partial_setoid_morphism_b ζp (weaken_right (hyperdoctrine_hyp _) _)) _). cbn. simplify_form. use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite conj_subst. use hyp_ltrans. use weaken_right. unfold w, x, y. clear w x y. simplify. pose (w := π₁ (π₁ (π₁ (tm_var (((W ×h X) ×h Y) ×h X))))). pose (x₁ := π₂ (π₁ (π₁ (tm_var (((W ×h X) ×h Y) ×h X))))). pose (y := π₂ (π₁ (tm_var (((W ×h X) ×h Y) ×h X)))). pose (x₂ := π₂ (tm_var (((W ×h X) ×h Y) ×h X))). fold w x₁ x₂ y. use (partial_setoid_mor_eq_defined ζ). + exact w. + exact x₂. + use weaken_left. use weaken_right. use (partial_setoid_mor_dom_defined ψ₁ w y). apply hyperdoctrine_hyp. + use partial_setoid_sym. use (partial_setoid_mono_eq φ Hφ). * exact y. * do 2 use weaken_left. apply hyperdoctrine_hyp. * do 2 use weaken_right. apply hyperdoctrine_hyp. + use weaken_right. 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.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.