Proposition is_pullback_subobject_classifier_partial_setoid_map_laws : partial_setoid_morphism_laws is_pullback_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. rewrite exists_subst. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. simplify_form. rewrite partial_setoid_subst. simplify. pose (w := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h W) ×h X) ×h Y))))). pose (x := π₂ (π₁ (tm_var (((𝟙 ×h W) ×h X) ×h Y)))). pose (y := π₂ (tm_var (((𝟙 ×h W) ×h X) ×h Y))). fold w x y. use weaken_right. use (partial_setoid_mor_dom_defined ψ₁ w y). apply hyperdoctrine_hyp. - unfold partial_setoid_mor_cod_defined_law ; cbn. do 2 use forall_intro. use impl_intro. use weaken_right. rewrite exists_subst. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. simplify_form. rewrite partial_setoid_subst. simplify. pose (w := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h W) ×h X) ×h Y))))). pose (x := π₂ (π₁ (tm_var (((𝟙 ×h W) ×h X) ×h Y)))). pose (y := π₂ (tm_var (((𝟙 ×h W) ×h X) ×h Y))). fold w x y. use weaken_left. use (partial_setoid_mor_dom_defined φ x y). apply hyperdoctrine_hyp. - unfold partial_setoid_mor_eq_defined_law ; cbn. do 4 use forall_intro. use impl_intro. use weaken_right. do 2 use impl_intro. use hyp_sym. rewrite exists_subst. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite conj_subst. use hyp_ltrans. use weaken_right. simplify_form. rewrite !partial_setoid_subst. simplify. pose (w₁ := π₂ (π₁ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h W) ×h W) ×h X) ×h X) ×h Y))))))). pose (w₂ := π₂ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h W) ×h W) ×h X) ×h X) ×h Y)))))). pose (x₁ := π₂ (π₁ (π₁ (tm_var (((((𝟙 ×h W) ×h W) ×h X) ×h X) ×h Y))))). pose (x₂ := π₂ (π₁ (tm_var (((((𝟙 ×h W) ×h W) ×h X) ×h X) ×h Y)))). pose (y := π₂ (tm_var (((((𝟙 ×h W) ×h W) ×h X) ×h X) ×h Y))). fold w₁ w₂ x₁ x₂ y. use exists_intro. { exact y. } simplify. fold x₂ w₂. use conj_intro. + use (partial_setoid_mor_eq_defined φ). * exact x₁. * exact y. * use weaken_left. use weaken_right. apply hyperdoctrine_hyp. * do 2 use weaken_right. use (partial_setoid_mor_cod_defined ψ₁ w₁). apply hyperdoctrine_hyp. * use weaken_right. use weaken_left. apply hyperdoctrine_hyp. + use (partial_setoid_mor_eq_defined ψ₁). * exact w₁. * exact y. * do 2 use weaken_left. apply hyperdoctrine_hyp. * do 2 use weaken_right. use (partial_setoid_mor_cod_defined ψ₁ w₁). apply hyperdoctrine_hyp. * do 2 use weaken_right. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_unique_im_law ; cbn. rewrite !exists_subst. do 3 use forall_intro. use impl_intro. use weaken_right. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. simplify_form. use impl_intro. use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite conj_subst. use hyp_ltrans. use weaken_right. simplify_form. rewrite partial_setoid_subst. simplify. pose (w := π₂ (π₁ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h W) ×h X) ×h X) ×h Y) ×h Y))))))). pose (x₁ := π₂ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h W) ×h X) ×h X) ×h Y) ×h Y)))))). pose (x₂ := π₂ (π₁ (π₁ (tm_var (((((𝟙 ×h W) ×h X) ×h X) ×h Y) ×h Y))))). pose (y₁ := π₂ (π₁ (tm_var (((((𝟙 ×h W) ×h X) ×h X) ×h Y) ×h Y)))). pose (y₂ := π₂ (tm_var (((((𝟙 ×h W) ×h X) ×h X) ×h Y) ×h Y))). fold w x₁ x₂ y₁ y₂. pose (Δ := (φ [⟨ x₁, y₁ ⟩] ∧ ψ₁ [⟨ w, y₁ ⟩]) ∧ φ [⟨ x₂, y₂ ⟩] ∧ ψ₁ [⟨ w, y₂ ⟩]). pose (Δ' := φ [⟨ x₁, y₁ ⟩] ∧ φ [⟨ x₂, y₁ ⟩]). assert (r : Δ ⊢ Δ'). { unfold Δ, Δ'. use conj_intro. + do 2 use weaken_left. apply hyperdoctrine_hyp. + 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_mor_unique_im ψ₁). ** exact w. ** do 2 use weaken_right. apply hyperdoctrine_hyp. ** use weaken_left. use weaken_right. apply hyperdoctrine_hyp. * use weaken_right. use weaken_left. apply hyperdoctrine_hyp. } refine (hyperdoctrine_cut r _). unfold Δ'. use (partial_setoid_mono_eq φ Hφ). + exact y₁. + use weaken_left. apply 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 (w := π₂ (tm_var (𝟙 ×h W))). fold w. pose (from_eq_partial_setoid_morphism_b q (t₁ := w) (t₂ := tripos_form_to_tm ⊤) (Δ := w ~ w)). cbn -[tripos_form_to_tm] in h. rewrite !exists_subst in h. use (exists_elim (h _)). + simplify. use exists_intro. { exact !!. } simplify. rewrite tripos_form_to_tm_Prf. use conj_intro ; [ | apply truth_intro ]. use (exists_elim (partial_setoid_mor_hom_exists ψ₂ (hyperdoctrine_hyp _))). use weaken_right. unfold w. simplify. use (hyperdoctrine_eq_transportf _ _ (hyperdoctrine_hyp _)). use hyperdoctrine_eq_pair_right. apply hyperdoctrine_unit_tm_eq. + unfold w. simplify_form. rewrite !partial_setoid_subst. simplify. rewrite <- hyperdoctrine_comp_subst. rewrite tripos_form_to_tm_Prf. simplify_form. refine (weaken_cut _ _). { do 3 use weaken_right. use (iff_elim_right (hyperdoctrine_hyp _)). apply truth_intro. } refine (exists_elim _ _). { use weaken_right. apply hyperdoctrine_hyp. } rewrite !conj_subst. use hyp_sym. use hyp_rtrans. use weaken_left. do 3 use hyp_rtrans. use weaken_left. simplify_form. rewrite !partial_setoid_subst. simplify. use exists_intro. { exact (π₂ (tm_var _)). } rewrite exists_subst. use exists_intro. { exact (π₂ (π₁ (tm_var _))). } simplify. clear w h. pose (x := π₂ (tm_var (((𝟙 ×h W) ×h Y) ×h X))). pose (y := π₂ (π₁ (tm_var (((𝟙 ×h W) ×h Y) ×h X)))). pose (w := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h W) ×h Y) ×h X))))). fold x y w. use conj_intro. * do 3 use weaken_left. apply hyperdoctrine_hyp. * 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.