Proposition proof_to_partial_setoid_morphism_laws {Γ₁ Γ₂ : ty H} {Δ : form Γ₁} {φ : form Γ₂} {s : tm Γ₁ Γ₂} (q : Δ ⊢ φ [ s ]) : partial_setoid_morphism_laws (proof_to_partial_setoid_morphism_form q). Proof. repeat split. - unfold partial_setoid_mor_dom_defined_law ; cbn. simplify. pose (x := π₂ (π₁ (tm_var ((𝟙 ×h Γ₁) ×h Γ₂)))). pose (y := π₂ (tm_var ((𝟙 ×h Γ₁) ×h Γ₂))). fold x y. do 2 use forall_intro. use impl_intro. use weaken_right. use eq_in_formula_to_partial_setoid. + apply hyperdoctrine_refl. + use weaken_left. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_cod_defined_law ; cbn. simplify. pose (x := π₂ (π₁ (tm_var ((𝟙 ×h Γ₁) ×h Γ₂)))). pose (y := π₂ (tm_var ((𝟙 ×h Γ₁) ×h Γ₂))). fold x y. do 2 use forall_intro. use impl_intro. use weaken_right. use eq_in_formula_to_partial_setoid. + apply hyperdoctrine_refl. + use weaken_right. use weaken_left. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_eq_defined_law ; cbn. simplify. pose (x₁ := π₂ (π₁ (π₁ (π₁ (tm_var ((((𝟙 ×h Γ₁) ×h Γ₁) ×h Γ₂) ×h Γ₂)))))). pose (x₂ := π₂ (π₁ (π₁ (tm_var ((((𝟙 ×h Γ₁) ×h Γ₁) ×h Γ₂) ×h Γ₂))))). pose (y₁ := π₂ (π₁ (tm_var ((((𝟙 ×h Γ₁) ×h Γ₁) ×h Γ₂) ×h Γ₂)))). pose (y₂ := π₂ (tm_var ((((𝟙 ×h Γ₁) ×h Γ₁) ×h Γ₂) ×h Γ₂))). fold x₁ x₂ y₁ y₂. do 4 use forall_intro. use impl_intro. use weaken_right. do 2 use impl_intro. use conj_intro. + do 2 use weaken_left. use hyperdoctrine_eq_transportf. * apply x₁. * exact (eq_from_formula_to_partial_setoid _ (hyperdoctrine_hyp _)). * exact (prop_from_formula_to_partial_setoid _ (hyperdoctrine_hyp _)). + use conj_intro. * use weaken_left. use weaken_right. use hyperdoctrine_eq_transportf. ** apply y₁. ** exact (eq_from_formula_to_partial_setoid _ (hyperdoctrine_hyp _)). ** exact (prop_from_formula_to_partial_setoid _ (hyperdoctrine_hyp _)). * use hyperdoctrine_eq_trans. ** exact y₁. ** use hyperdoctrine_eq_sym. use weaken_left. use weaken_right. exact (eq_from_formula_to_partial_setoid _ (hyperdoctrine_hyp _)). ** use hyperdoctrine_eq_trans. *** exact (s [ x₁ ]tm). *** do 3 use weaken_right. apply hyperdoctrine_hyp. *** use hyperdoctrine_subst_eq. do 2 use weaken_left. exact (eq_from_formula_to_partial_setoid _ (hyperdoctrine_hyp _)). - unfold partial_setoid_mor_unique_im_law ; cbn. simplify. pose (x := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h Γ₁) ×h Γ₂) ×h Γ₂))))). pose (y₁ := π₂ (π₁ (tm_var (((𝟙 ×h Γ₁) ×h Γ₂) ×h Γ₂)))). pose (y₂ := π₂ (tm_var (((𝟙 ×h Γ₁) ×h Γ₂) ×h Γ₂))). fold x y₁ y₂. do 3 use forall_intro. use impl_intro. use weaken_right. use impl_intro. use eq_in_formula_to_partial_setoid. + use hyperdoctrine_eq_trans. * exact (s [ x ]tm). * use weaken_left. do 2 use weaken_right. apply hyperdoctrine_hyp. * use hyperdoctrine_eq_sym. do 3 use weaken_right. apply hyperdoctrine_hyp. + use weaken_left. 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 (s [ π₂ (tm_var (𝟙 ×h Γ₁)) ]tm). + simplify. pose (x := π₂ (tm_var (𝟙 ×h Γ₁))). fold x. use conj_intro. * exact (prop_from_formula_to_partial_setoid _ (hyperdoctrine_hyp _)). * use conj_intro. ** refine (hyperdoctrine_cut (prop_from_formula_to_partial_setoid _ (hyperdoctrine_hyp _)) _). refine (hyperdoctrine_cut (hyperdoctrine_proof_subst x q) _). simplify. apply hyperdoctrine_hyp. ** apply hyperdoctrine_refl. 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.