Proposition formula_to_partial_setoid_incl_laws {A : ty H} (φ : form A) : partial_setoid_morphism_laws (formula_to_partial_setoid_incl_form φ). Proof. repeat split. - unfold partial_setoid_mor_dom_defined_law ; cbn. simplify. pose (x₁ := π₂ (π₁ (tm_var ((𝟙 ×h A) ×h A)))). pose (x₂ := π₂ (tm_var ((𝟙 ×h A) ×h A))). fold x₁ x₂. do 2 use forall_intro. use impl_intro. use weaken_right. use eq_in_formula_to_partial_setoid. + use hyperdoctrine_refl. + use weaken_right. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_cod_defined_law ; cbn. simplify. pose (x₁ := π₂ (π₁ (tm_var ((𝟙 ×h A) ×h A)))). pose (x₂ := π₂ (tm_var ((𝟙 ×h A) ×h A))). fold x₁ x₂. do 2 use forall_intro. use impl_intro. use weaken_right. use eq_in_eq_partial_setoid. use hyperdoctrine_refl. - unfold partial_setoid_mor_eq_defined_law ; cbn. simplify. pose (x₁ := π₂ (π₁ (π₁ (π₁ (tm_var ((((𝟙 ×h A) ×h A) ×h A) ×h A)))))). pose (x₂ := π₂ (π₁ (π₁ (tm_var ((((𝟙 ×h A) ×h A) ×h A) ×h A))))). pose (x₃ := π₂ (π₁ (tm_var ((((𝟙 ×h A) ×h A) ×h A) ×h A)))). pose (x₄ := π₂ (tm_var ((((𝟙 ×h A) ×h A) ×h A) ×h A))). fold x₁ x₂ x₃ x₄. do 4 use forall_intro. use impl_intro. use weaken_right. do 2 use impl_intro. use conj_intro. + use hyp_rtrans. use weaken_left. use hyperdoctrine_eq_trans. * exact x₁. * do 2 use weaken_left. use hyperdoctrine_eq_sym. use (eq_from_formula_to_partial_setoid φ). apply hyperdoctrine_hyp. * use hyperdoctrine_eq_trans. ** exact x₃. ** use weaken_right. apply hyperdoctrine_hyp. ** use weaken_left. use weaken_right. use from_eq_in_eq_partial_setoid. apply hyperdoctrine_hyp. + use hyperdoctrine_eq_transportf. * exact x₁. * do 2 use weaken_left. exact (eq_from_formula_to_partial_setoid _ (hyperdoctrine_hyp _)). * do 2 use weaken_right. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_unique_im_law ; cbn. simplify. pose (x₁ := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h A) ×h A) ×h A))))). pose (x₂ := π₂ (π₁ (tm_var (((𝟙 ×h A) ×h A) ×h A)))). pose (x₃ := π₂ (tm_var (((𝟙 ×h A) ×h A) ×h A))). fold x₁ x₂ x₃. do 3 use forall_intro. use impl_intro. use weaken_right. use impl_intro. use eq_in_eq_partial_setoid. use hyperdoctrine_eq_trans. + exact x₁. + use hyperdoctrine_eq_sym. do 2 use weaken_left. apply hyperdoctrine_hyp. + use weaken_right. use weaken_left. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_hom_exists_law ; cbn. simplify. use forall_intro. use impl_intro. use weaken_right. use exists_intro. + exact (π₂ (tm_var _)). + simplify. pose (x := π₂ (tm_var (𝟙 ×h A))). fold x. use conj_intro. * use (eq_from_formula_to_partial_setoid φ). apply hyperdoctrine_hyp. * exact (prop_from_formula_to_partial_setoid φ (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.