Definition dispBinProducts_poset_disp_cat : dispBinProducts poset_disp_cat BinProductsHSET. Proof. intros X₁ X₂ R₁ R₂. use make_dispBinProduct_locally_prop. - exact poset_disp_cat_locally_prop. - exists (prod_PartialOrder R₁ R₂). split ; cbn. + exact (dirprod_pr1_is_monotone R₁ R₂). + exact (dirprod_pr2_is_monotone R₁ R₂). - cbn. intros W f g RW Hf Hg. exact (prodtofun_is_monotone Hf Hg). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.DisplayedCats.Binproducts. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Categories.HSET.All.