Proposition preserves_binproduct_functor_to_partial_setoids_inv_left : partial_setoid_comp_morphism preserves_binproduct_functor_to_partial_setoids_inv φ = id_partial_setoid_morphism _. Proof. unfold φ. assert (BinProductPr1 (hyperdoctrine_type_category H) (hyperdoctrine_binproducts H X Y) = π₁ (tm_var _)) as q. { unfold hyperdoctrine_pr1, tm_var. rewrite id_left. apply idpath. } rewrite q ; clear q. assert (BinProductPr2 (hyperdoctrine_type_category H) (hyperdoctrine_binproducts H X Y) = π₂ (tm_var _)) as q. { unfold hyperdoctrine_pr2, tm_var. rewrite id_left. apply idpath. } rewrite q ; clear q. use eq_partial_setoid_morphism. - use (exists_elim (hyperdoctrine_hyp _)) ; cbn. use weaken_right. simplify_form. rewrite partial_setoid_subst. simplify. pose (xy₁ := π₁ (π₁ (tm_var (((X ×h Y) ×h X ×h Y) ×h X ×h Y)))). pose (xy₂ := π₂ (π₁ (tm_var (((X ×h Y) ×h X ×h Y) ×h X ×h Y)))). pose (xy₃ := π₂ (tm_var (((X ×h Y) ×h X ×h Y) ×h X ×h Y))). cbn. fold xy₁ xy₂ xy₃. use eq_in_prod_partial_setoid. + use eq_in_eq_partial_setoid. simple refine (hyperdoctrine_eq_trans _ _). * exact (π₁ xy₃). * use weaken_left. use hyperdoctrine_eq_pr1. apply hyperdoctrine_hyp. * use weaken_right. use weaken_left. apply hyperdoctrine_hyp. + use eq_in_eq_partial_setoid. simple refine (hyperdoctrine_eq_trans _ _). * exact (π₂ xy₃). * use weaken_left. use hyperdoctrine_eq_pr2. apply hyperdoctrine_hyp. * do 2 use weaken_right. apply hyperdoctrine_hyp. - cbn. use exists_intro. + exact (π₁ (tm_var _)). + simplify. repeat (use conj_intro). * apply hyperdoctrine_refl. * 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 _)). 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.