Proposition lam_partial_setoid_laws : partial_setoid_morphism_laws lam_partial_setoid_form. Proof. repeat split. - unfold partial_setoid_mor_dom_defined_law ; cbn. simplify_form. use forall_intro. use forall_intro. use impl_intro. use weaken_right. pose (z := π₂ (π₁ (tm_var ((𝟙 ×h Z) ×h ℙ (X ×h Y))))). pose (f := π₂ (tm_var ((𝟙 ×h Z) ×h ℙ (X ×h Y)))). fold z f. use (lam_partial_setoid_form_def_dom z f). apply hyperdoctrine_hyp. - unfold partial_setoid_mor_cod_defined_law ; cbn. simplify_form. do 2 use forall_intro. use impl_intro. use weaken_right. pose (z := π₂ (π₁ (tm_var ((𝟙 ×h Z) ×h ℙ (X ×h Y))))). pose (f := π₂ (tm_var ((𝟙 ×h Z) ×h ℙ (X ×h Y)))). fold z f. use eq_in_exp_partial_setoid. + use (lam_partial_setoid_form_is_function z f). apply hyperdoctrine_hyp. + use (lam_partial_setoid_form_def_fun z f). 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. pose (Γ := (((𝟙 ×h Z) ×h Z) ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y)). pose (f' := π₂ (tm_var Γ)). pose (f := π₂ (π₁ (tm_var Γ))). pose (z' := π₂ (π₁ (π₁ (tm_var Γ)))). pose (z := π₂ (π₁ (π₁ (π₁ (tm_var Γ))))). unfold Γ in * ; clear Γ. fold f f' z z'. use to_lam_partial_setoid_eq. + refine (partial_setoid_refl_r _). do 2 use weaken_left. apply hyperdoctrine_hyp. + use exp_partial_setoid_eq_is_function. * exact f. * use weaken_left. use weaken_right. use from_eq_in_exp_partial_setoid_function_eq. apply hyperdoctrine_hyp. * use weaken_right. use (lam_partial_setoid_form_is_function z f). apply hyperdoctrine_hyp. + unfold lam_partial_setoid_eq. simplify_form. do 2 use forall_intro. unfold f', f, z', z ; cbn ; clear f' f z' z. simplify_form. rewrite !partial_setoid_subst. simplify. pose (Γ := (((((𝟙 ×h Z) ×h Z) ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y)) ×h X) ×h Y). pose (y := π₂ (tm_var Γ)). pose (x := π₂ (π₁ (tm_var Γ))). pose (f' := π₂ (π₁ (π₁ (tm_var Γ)))). pose (f := π₂ (π₁ (π₁ (π₁ (tm_var Γ))))). pose (z' := π₂ (π₁ (π₁ (π₁ (π₁ (tm_var Γ)))))). pose (z := π₂ (π₁ (π₁ (π₁ (π₁ (π₁ (tm_var Γ))))))). unfold Γ in * ; clear Γ ; cbn. fold x y z z' f f'. use iff_intro. * use from_exp_partial_setoid_eq. ** exact f. ** do 2 use weaken_left. use weaken_right. use from_eq_in_exp_partial_setoid_function_eq. apply hyperdoctrine_hyp. ** refine (lam_partial_setoid_eq_left z f _ x y _). *** use weaken_left. use weaken_right. apply hyperdoctrine_hyp. *** use (partial_setoid_mor_eq_defined φ). **** exact ⟨ x , z' ⟩. **** exact y. **** use eq_in_prod_partial_setoid ; simplify. { use weaken_right. refine (hyperdoctrine_cut (partial_setoid_mor_dom_defined φ ⟨ x , z' ⟩ y (hyperdoctrine_hyp _)) _). refine (hyperdoctrine_cut (eq_in_prod_partial_setoid_l _ _ (hyperdoctrine_hyp _)) _). simplify. apply hyperdoctrine_hyp. } do 3 use weaken_left. use partial_setoid_sym. apply hyperdoctrine_hyp. **** use weaken_right. exact (partial_setoid_mor_cod_defined φ ⟨ x , z' ⟩ y (hyperdoctrine_hyp _)). **** use weaken_right. apply hyperdoctrine_hyp. * refine (lam_partial_setoid_eq_right z' f _ x y _). ** use lam_partial_setoid_eq_arg. *** exact z. *** do 3 use weaken_left. apply hyperdoctrine_hyp. *** do 2 use weaken_left. use weaken_right. exact (partial_setoid_refl_l (hyperdoctrine_hyp _)). *** use weaken_left. use weaken_right. apply hyperdoctrine_hyp. ** use from_exp_partial_setoid_eq. *** exact f'. *** do 2 use weaken_left. use weaken_right. use from_eq_in_exp_partial_setoid_function_eq. use partial_setoid_sym. apply hyperdoctrine_hyp. *** use weaken_right. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_unique_im_law ; cbn -[lam_partial_setoid_form]. do 3 use forall_intro. use impl_intro. use weaken_right. use impl_intro. pose (z := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h Z) ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y)))))). pose (f := π₂ (π₁ (tm_var (((𝟙 ×h Z) ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y))))). pose (g := π₂ (tm_var (((𝟙 ×h Z) ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y)))). fold z f g. simplify. use eq_in_exp_partial_setoid. + use weaken_left. use (lam_partial_setoid_form_is_function z f). apply hyperdoctrine_hyp. + unfold exp_partial_setoid_eq, f, g, z ; clear f g z. simplify. do 2 use forall_intro. simplify. pose (Γ := ((((𝟙 ×h Z) ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y)) ×h X) ×h Y). pose (x := π₂ (π₁ (tm_var Γ))). pose (y := π₂ (tm_var Γ)). pose (f := π₂ (π₁ (π₁ (tm_var Γ)))). pose (g := π₂ (π₁ (π₁ (π₁ (tm_var Γ))))). pose (z := π₂ (π₁ (π₁ (π₁ (π₁ (tm_var Γ)))))). unfold Γ in * ; clear Γ. fold x y z f g. refine (iff_trans _ _). { use iff_sym. use (lam_partial_setoid_eq_iff z g). use weaken_left. apply hyperdoctrine_hyp. } use (lam_partial_setoid_eq_iff z f). use weaken_right. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_hom_exists_law ; cbn. use forall_intro. use impl_intro. use weaken_right. simplify. use exists_intro. + exact {{ lam_image_form }}. + pose (z := π₂ (tm_var (𝟙 ×h Z))). simplify. fold z. use to_lam_partial_setoid_eq. * apply hyperdoctrine_hyp. * apply is_function_lam_image_form. fold z. apply hyperdoctrine_hyp. * apply lam_partial_setoid_eq_image_form. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. 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.PERBinProducts. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.ExponentialPER.