Proposition subobject_classifier_partial_setoid_comm : partial_setoid_comp_morphism φ subobject_classifier_partial_setoid_map = partial_setoid_comp_morphism (partial_setoid_morphism_to_terminal X) omega_partial_setoid_true. Proof. use eq_partial_setoid_morphism ; cbn. - use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. rewrite exists_subst. use exists_intro. { exact !!. } simplify_form. rewrite !partial_setoid_subst. simplify. pose (x := π₁ (π₁ (tm_var ((X ×h Ω) ×h Y)))). pose (ω := π₂ (π₁ (tm_var ((X ×h Ω) ×h Y)))). pose (y := π₂ (tm_var ((X ×h Ω) ×h Y))). fold x ω y. use conj_intro. + use (partial_setoid_mor_dom_defined φ). * exact y. * use weaken_left. apply hyperdoctrine_hyp. + use (iff_elim_left (weaken_right (weaken_right (hyperdoctrine_hyp _) _) _)). use exists_intro. * exact x. * simplify. use weaken_left. apply hyperdoctrine_hyp. - use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. rewrite partial_setoid_subst. simplify. use (exists_elim (partial_setoid_mor_hom_exists φ (weaken_left (hyperdoctrine_hyp _) _))). rewrite exists_subst. use exists_intro. { exact (π₂ (tm_var _)). } simplify_form. rewrite !partial_setoid_subst. simplify. pose (x := π₁ (π₁ (π₁ (tm_var (((X ×h Ω) ×h 𝟙) ×h Y))))). pose (ω := π₂ (π₁ (π₁ (tm_var (((X ×h Ω) ×h 𝟙) ×h Y))))). pose (y := π₂ (tm_var (((X ×h Ω) ×h 𝟙) ×h Y))). fold x ω y. repeat use conj_intro. + use weaken_right. apply hyperdoctrine_hyp. + use (partial_setoid_mor_cod_defined φ). * exact x. * use weaken_right. apply hyperdoctrine_hyp. + use impl_intro. do 2 use weaken_left. use weaken_right. apply hyperdoctrine_hyp. + use impl_intro. use exists_intro. * exact x. * simplify. use weaken_left. 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.