Proposition subobject_classifier_partial_setoid_map_laws : partial_setoid_morphism_laws subobject_classifier_partial_setoid_map_form. Proof. repeat split. - unfold partial_setoid_mor_dom_defined_law ; cbn. do 2 (use forall_intro). use impl_intro. use weaken_right. simplify_form. rewrite !partial_setoid_subst. simplify. pose (y := π₂ (π₁ (tm_var ((𝟙 ×h Y) ×h Ω)))). pose (ω := π₂ (tm_var ((𝟙 ×h Y) ×h Ω))). fold y ω. use weaken_left. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_cod_defined_law ; cbn. do 2 (use forall_intro). use impl_intro. use weaken_right. simplify_form. rewrite partial_setoid_subst. simplify. pose (y := π₂ (π₁ (tm_var ((𝟙 ×h Y) ×h Ω)))). pose (ω := π₂ (tm_var ((𝟙 ×h Y) ×h Ω))). fold y ω. use eq_in_omega_partial_setoid. apply iff_refl. - unfold partial_setoid_mor_eq_defined_law ; cbn. do 4 use forall_intro. use impl_intro. use weaken_right. do 2 use impl_intro. simplify_form. rewrite !partial_setoid_subst. simplify. pose (y₁ := π₂ (π₁ (π₁ (π₁ (tm_var ((((𝟙 ×h Y) ×h Y) ×h Ω) ×h Ω)))))). pose (y₂ := π₂ (π₁ (π₁ (tm_var ((((𝟙 ×h Y) ×h Y) ×h Ω) ×h Ω))))). pose (ω₁ := π₂ (π₁ (tm_var ((((𝟙 ×h Y) ×h Y) ×h Ω) ×h Ω)))). pose (ω₂ := π₂ (tm_var ((((𝟙 ×h Y) ×h Y) ×h Ω) ×h Ω))). fold y₁ y₂ ω₁ ω₂. use conj_intro. + do 2 use weaken_left. exact (partial_setoid_refl_r (hyperdoctrine_hyp _)). + use iff_intro. * use (from_eq_in_omega_partial_setoid_left (ω₁ := ω₁) (ω₂ := ω₂)). ** do 2 use weaken_left. use weaken_right. apply hyperdoctrine_hyp. ** use (iff_elim_left (weaken_left (weaken_right (weaken_right (hyperdoctrine_hyp _) _) _) _)). use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite conj_subst. use hyp_ltrans. use weaken_right. simplify_form. unfold y₁, y₂, ω₁, ω₂ ; clear y₁ y₂ ω₁ ω₂. rewrite !partial_setoid_subst. simplify. pose (y₁ := π₂ (π₁ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h Y) ×h Y) ×h Ω) ×h Ω) ×h X))))))). pose (y₂ := π₂ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h Y) ×h Y) ×h Ω) ×h Ω) ×h X)))))). pose (ω₁ := π₂ (π₁ (π₁ (tm_var (((((𝟙 ×h Y) ×h Y) ×h Ω) ×h Ω) ×h X))))). pose (ω₂ := π₂ (π₁ (tm_var (((((𝟙 ×h Y) ×h Y) ×h Ω) ×h Ω) ×h X)))). pose (x := π₂ (tm_var (((((𝟙 ×h Y) ×h Y) ×h Ω) ×h Ω) ×h X))). cbn. fold y₁ y₂ ω₁ ω₂ x. use exists_intro. { exact x. } simplify. fold y₁. use (partial_setoid_mor_eq_defined φ). *** exact x. *** exact y₂. *** use weaken_right. use (partial_setoid_mor_dom_defined φ x y₂). apply hyperdoctrine_hyp. *** use partial_setoid_sym. do 3 use weaken_left. apply hyperdoctrine_hyp. *** use weaken_right. apply hyperdoctrine_hyp. * use weaken_cut. ** exact (∃h (φ [⟨ π₂ (tm_var _) , π₂ (π₁ (π₁ (π₁ (π₁ (tm_var _))))) ⟩])). ** use iff_elim_right. *** exact (Prf [ ω₁ ]). *** use weaken_left. do 2 use weaken_right. apply hyperdoctrine_hyp. *** use from_eq_in_omega_partial_setoid_left. **** exact ω₂. **** do 2 use weaken_left. use weaken_right. use partial_setoid_sym. apply hyperdoctrine_hyp. **** use weaken_right. apply hyperdoctrine_hyp. ** use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite conj_subst. use hyp_ltrans. use weaken_right. simplify_form. unfold y₁, y₂, ω₁, ω₂ ; clear y₁ y₂ ω₁ ω₂. rewrite !partial_setoid_subst. simplify. pose (y₁ := π₂ (π₁ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h Y) ×h Y) ×h Ω) ×h Ω) ×h X))))))). pose (y₂ := π₂ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h Y) ×h Y) ×h Ω) ×h Ω) ×h X)))))). pose (ω₁ := π₂ (π₁ (π₁ (tm_var (((((𝟙 ×h Y) ×h Y) ×h Ω) ×h Ω) ×h X))))). pose (ω₂ := π₂ (π₁ (tm_var (((((𝟙 ×h Y) ×h Y) ×h Ω) ×h Ω) ×h X)))). pose (x := π₂ (tm_var (((((𝟙 ×h Y) ×h Y) ×h Ω) ×h Ω) ×h X))). cbn. fold y₁ y₂ ω₁ ω₂ x. use exists_intro. { exact x. } simplify. fold y₂. use (partial_setoid_mor_eq_defined φ _ _ (weaken_right (hyperdoctrine_hyp _) _)). *** use weaken_right. use (partial_setoid_mor_dom_defined φ x y₁). apply hyperdoctrine_hyp. *** do 4 use weaken_left. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_unique_im_law ; cbn. do 3 use forall_intro. use impl_intro. use weaken_right. simplify_form. rewrite !partial_setoid_subst. simplify. pose (y := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h Y) ×h Ω) ×h Ω))))). pose (ω₁ := π₂ (π₁ (tm_var (((𝟙 ×h Y) ×h Ω) ×h Ω)))). pose (ω₂ := π₂ (tm_var (((𝟙 ×h Y) ×h Ω) ×h Ω))). fold y ω₁ ω₂. use impl_intro. use eq_in_omega_partial_setoid. use iff_intro. + use (iff_elim_left (weaken_left (weaken_right (weaken_right (hyperdoctrine_hyp _) _) _) _)). use (iff_elim_right (weaken_left (weaken_left (weaken_right (hyperdoctrine_hyp _) _) _) _)). use weaken_right. apply hyperdoctrine_hyp. + use (iff_elim_left (weaken_left (weaken_left (weaken_right (hyperdoctrine_hyp _) _) _) _)). use (iff_elim_right (weaken_left (weaken_right (weaken_right (hyperdoctrine_hyp _) _) _) _)). use weaken_right. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_hom_exists_law ; cbn. use forall_intro. use impl_intro. use weaken_right. pose (y := π₂ (tm_var (𝟙 ×h Y))). fold y. use exists_intro. { exact (tripos_form_to_tm (∃h (φ [ ⟨ π₂ (tm_var _) , π₂ (π₁ (tm_var _)) ⟩ ]))). } simplify_form. rewrite partial_setoid_subst. unfold y. simplify. rewrite tripos_form_to_tm_Prf. use conj_intro. + apply hyperdoctrine_hyp. + apply iff_refl. 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.