Definition preserves_binproduct_functor_to_partial_setoids (H : first_order_hyperdoctrine) : preserves_binproduct (functor_to_partial_setoids H). Proof. use preserves_binproduct_chosen_to_chosen. - exact (hyperdoctrine_binproducts H). - exact (binproducts_partial_setoid H). - intros X Y. use make_is_z_isomorphism. + apply preserves_binproduct_functor_to_partial_setoids_inv. + abstract (split ; [ apply preserves_binproduct_functor_to_partial_setoids_inv_right | apply preserves_binproduct_functor_to_partial_setoids_inv_left ]). Defined.
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.