Proposition poset_to_underlying_binary_prod_map_monotone {φ₁ φ₂ : x --> y₁} {ψ₁ ψ₂ : x --> y₂} (p : E x y₁ φ₁ φ₂) (q : E x y₂ ψ₁ ψ₂) : E _ _ (poset_to_underlying_binary_prod_map φ₁ ψ₁) (poset_to_underlying_binary_prod_map φ₂ ψ₂). Proof. exact (pr2 (@BinProductArrow _ _ _ (is_binary_prod_enriched_to_BinProduct E' _ _ (pr2 (EP y₁ y₂)) x) prod prod_pr1 prod_pr2) (φ₁ ,, ψ₁) (φ₂ ,, ψ₂) (p ,, q)). Qed.
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.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.CategoryOfPosets. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.PosetEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedTerminal. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedBinaryProducts. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedProducts. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedEqualizers. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedPowers. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.CategoryTheory.Monoidal.Structure.Cartesian. Require Import UniMath.CategoryTheory.Monoidal.Examples.PosetsMonoidal. Require Import UniMath.CategoryTheory.Monoidal.Examples.CartesianMonoidal. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Equalizers. Import MonoidalNotations.