Proposition partial_setoids_disp_functor_eso_mor_laws : partial_setoid_morphism_laws partial_setoids_disp_functor_eso_mor_form. Proof. unfold partial_setoids_disp_functor_eso_mor_form. repeat split. - unfold partial_setoid_mor_dom_defined_law ; cbn. do 2 use forall_intro. use impl_intro. use weaken_right. simplify. use eq_in_formula_to_partial_setoid. + apply hyperdoctrine_refl. + simplify_form. use exists_intro. * exact (π₂ (tm_var _)). * simplify. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_cod_defined_law ; cbn. do 2 use forall_intro. use impl_intro. use weaken_right. simplify. exact (partial_setoid_mor_dom_defined φ _ _ (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. simplify. refine (partial_setoid_mor_eq_defined φ _ _ (weaken_right (hyperdoctrine_hyp _) _)). + use weaken_left. use weaken_right. apply hyperdoctrine_hyp. + do 2 use weaken_left ; cbn. use eq_in_eq_partial_setoid. exact (eq_from_formula_to_partial_setoid _ (hyperdoctrine_hyp _)). - unfold partial_setoid_mor_unique_im_law ; cbn. do 3 use forall_intro. use impl_intro. use weaken_right. use impl_intro. simplify. pose (x₁ := π₂ (π₁ (tm_var (((𝟙 ×h A) ×h X) ×h X)))). pose (x₂ := π₂ (tm_var (((𝟙 ×h A) ×h X) ×h X))). pose (a := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h A) ×h X) ×h X))))). pose (Δ := φ [⟨ x₁ , a ⟩] ∧ φ [⟨ x₂ , a ⟩]). fold x₁ x₂ a. assert (Δ ⊢ x₁ ~ x₁) as r₁. { unfold Δ. use (partial_setoid_mor_dom_defined φ _ a). use weaken_left. apply hyperdoctrine_hyp. } assert (Δ ⊢ x₂ ~ x₂) as r₂. { unfold Δ. use (partial_setoid_mor_dom_defined φ _ a). use weaken_right. apply hyperdoctrine_hyp. } enough (partial_setoid_comp_morphism (point_partial_setoid_morphism Δ x₁ r₁) φ = partial_setoid_comp_morphism (point_partial_setoid_morphism Δ x₂ r₂) φ) as r₃. { pose (Hφ _ _ _ r₃) as p. refine (hyperdoctrine_cut (@from_eq_partial_setoid_morphism_f _ _ _ _ _ p _ Δ (tm_var _) x₁ _) _). + cbn. unfold Δ. simplify_form. rewrite partial_setoid_subst. simplify. use conj_intro. * apply hyperdoctrine_hyp. * use weaken_left. use (partial_setoid_mor_dom_defined φ x₁ a). apply hyperdoctrine_hyp. + cbn. unfold Δ. simplify_form. rewrite partial_setoid_subst. simplify. use weaken_right. apply hyperdoctrine_hyp. } use eq_partial_setoid_morphism ; cbn. + use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. simplify_form. use exists_intro. * exact (π₂ (π₁ (π₁ (tm_var _)))). * rewrite !partial_setoid_subst. simplify. unfold x₁, x₂. rewrite !partial_setoid_subst. simplify. repeat (use conj_intro). ** do 2 use weaken_left. apply hyperdoctrine_hyp. ** unfold Δ, x₁, x₂. rewrite !conj_subst. do 2 use weaken_left. use weaken_right. simplify. exact (partial_setoid_mor_dom_defined φ _ _ (hyperdoctrine_hyp _)). ** unfold Δ, x₁, a, x₂ ; clear Δ x₁ a x₂ r₁ r₂. simplify. pose (a₁ := π₂ (π₁ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h A) ×h X) ×h X) ×h A) ×h X))))))). pose (x₁ := π₂ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h A) ×h X) ×h X) ×h A) ×h X)))))). pose (x₂ := π₂ (π₁ (π₁ (tm_var (((((𝟙 ×h A) ×h X) ×h X) ×h A) ×h X))))). pose (a₂ := π₂ (π₁ (tm_var (((((𝟙 ×h A) ×h X) ×h X) ×h A) ×h X)))). pose (x₃ := π₂ (tm_var (((((𝟙 ×h A) ×h X) ×h X) ×h A) ×h X))). cbn. fold a₁ a₂ x₁ x₂ x₃. use (partial_setoid_mor_eq_defined φ). *** exact x₂. *** exact a₁. *** do 2 use weaken_left. use weaken_right. exact (partial_setoid_mor_dom_defined φ _ _ (hyperdoctrine_hyp _)). *** use (partial_setoid_mor_unique_im φ). **** exact x₁. **** do 3 use weaken_left. apply hyperdoctrine_hyp. **** do 2 use hyp_ltrans. do 2 use weaken_right. pose (Δ := x₃ ~ x₁ ∧ φ [⟨ x₃ , a₂ ⟩]). assert (Δ ⊢ x₃ ~ x₁) as q₁. { use weaken_left. apply hyperdoctrine_hyp. } assert (Δ ⊢ (a₂ : tm _ (eq_partial_setoid _)) ~ a₂) as q₂. { use weaken_right. exact (partial_setoid_mor_cod_defined φ _ _ (hyperdoctrine_hyp _)). } use (partial_setoid_mor_eq_defined φ q₁ q₂). use weaken_right. apply hyperdoctrine_hyp. *** do 2 use weaken_left. use weaken_right. apply hyperdoctrine_hyp. + use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. simplify_form. use exists_intro. * exact (π₂ (π₁ (π₁ (π₁ (tm_var _))))). * rewrite !partial_setoid_subst. simplify. rewrite !partial_setoid_subst. simplify. unfold x₁, x₂. simplify. repeat (use conj_intro). ** do 2 use weaken_left. apply hyperdoctrine_hyp. ** unfold Δ, x₁, x₂. do 2 use weaken_left. rewrite conj_subst. use weaken_left. simplify. exact (partial_setoid_mor_dom_defined φ _ _ (hyperdoctrine_hyp _)). ** unfold Δ, x₁, a, x₂. simplify. clear Δ x₁ a x₂ r₁ r₂. pose (a₁ := π₂ (π₁ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h A) ×h X) ×h X) ×h A) ×h X))))))). pose (x₁ := π₂ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h A) ×h X) ×h X) ×h A) ×h X)))))). pose (x₂ := π₂ (π₁ (π₁ (tm_var (((((𝟙 ×h A) ×h X) ×h X) ×h A) ×h X))))). pose (a₂ := π₂ (π₁ (tm_var (((((𝟙 ×h A) ×h X) ×h X) ×h A) ×h X)))). pose (x₃ := π₂ (tm_var (((((𝟙 ×h A) ×h X) ×h X) ×h A) ×h X))). cbn. fold a₁ a₂ x₁ x₂ x₃. use (partial_setoid_mor_eq_defined φ). *** exact x₁. *** exact a₁. *** do 3 use weaken_left. exact (partial_setoid_mor_dom_defined φ _ _ (hyperdoctrine_hyp _)). *** use (partial_setoid_mor_unique_im φ). **** exact x₂. **** do 2 use weaken_left. use weaken_right. apply hyperdoctrine_hyp. **** do 2 use hyp_ltrans. do 2 use weaken_right. pose (Δ := x₃ ~ x₂ ∧ φ [⟨ x₃ , a₂ ⟩]). assert (Δ ⊢ x₃ ~ x₂) as q₁. { use weaken_left. apply hyperdoctrine_hyp. } assert (Δ ⊢ (a₂ : tm _ (eq_partial_setoid _)) ~ a₂) as q₂. { use weaken_right. exact (partial_setoid_mor_cod_defined φ _ _ (hyperdoctrine_hyp _)). } use (partial_setoid_mor_eq_defined φ q₁ q₂). use weaken_right. apply hyperdoctrine_hyp. *** do 3 use weaken_left. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_hom_exists_law ; cbn. use forall_intro. use impl_intro. use weaken_right. simplify. unfold partial_setoid_formula. cbn. simplify. 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.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.MonoCodomain. Require Import UniMath.CategoryTheory.DisplayedCats.MonoCodomain.FiberMonoCod. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. 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.PERConstantObjects.