Proposition preserves_binproduct_functor_to_partial_setoids_inv_laws : partial_setoid_morphism_laws preserves_binproduct_functor_to_partial_setoids_inv_form. Proof. repeat split. - unfold partial_setoid_mor_dom_defined_law ; cbn. do 2 (use forall_intro). use impl_intro. use weaken_right. use eq_in_prod_partial_setoid. + use eq_in_eq_partial_setoid. apply hyperdoctrine_refl. + use eq_in_eq_partial_setoid. apply hyperdoctrine_refl. - unfold partial_setoid_mor_cod_defined_law ; cbn. do 2 (use forall_intro). use impl_intro. use weaken_right. use eq_in_eq_partial_setoid. apply hyperdoctrine_refl. - 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. pose (xy₁ := π₂ (π₁ (π₁ (π₁ (tm_var ((((𝟙 ×h X ×h Y) ×h X ×h Y) ×h X ×h Y) ×h X ×h Y)))))). pose (xy₂ := π₂ (π₁ (π₁ (tm_var ((((𝟙 ×h X ×h Y) ×h X ×h Y) ×h X ×h Y) ×h X ×h Y))))). pose (xy₃ := π₂ (π₁ (tm_var ((((𝟙 ×h X ×h Y) ×h X ×h Y) ×h X ×h Y) ×h X ×h Y)))). pose (xy₄ := π₂ (tm_var ((((𝟙 ×h X ×h Y) ×h X ×h Y) ×h X ×h Y) ×h X ×h Y))). fold xy₁ xy₂ xy₃ xy₄. use hyperdoctrine_eq_trans. + exact xy₁. + do 2 use weaken_left. use hyperdoctrine_eq_sym. use hyperdoctrine_eq_prod_eq. * use from_eq_in_eq_partial_setoid. exact (eq_in_prod_partial_setoid_l _ _ (hyperdoctrine_hyp _)). * use from_eq_in_eq_partial_setoid. exact (eq_in_prod_partial_setoid_r _ _ (hyperdoctrine_hyp _)). + use hyperdoctrine_eq_trans. * exact xy₃. * use weaken_right. apply hyperdoctrine_hyp. * use weaken_left. use weaken_right. use from_eq_in_eq_partial_setoid. apply 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 (xy₁ := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h X ×h Y) ×h X ×h Y) ×h X ×h Y))))). pose (xy₂ := π₂ (π₁ (tm_var (((𝟙 ×h X ×h Y) ×h X ×h Y) ×h X ×h Y)))). pose (xy₃ := π₂ (tm_var (((𝟙 ×h X ×h Y) ×h X ×h Y) ×h X ×h Y))). fold xy₁ xy₂ xy₃. use eq_in_eq_partial_setoid. use hyperdoctrine_eq_trans. + exact xy₁. + use hyperdoctrine_eq_sym. 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. use exists_intro. + exact (π₂ (tm_var _)). + simplify. apply hyperdoctrine_refl. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Preservation. 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.