Definition poset_enrichment_prod_is_prod : is_prod_enriched E' ys make_poset_enriched_prod_cone. Proof. use make_is_prod_enriched. - intros z P fs. refine (_ · poset_enrichment_prod_pair _ _ _). simple refine (_ ,, _). + exact (λ x j, pr1 (fs j) x). + abstract (use is_monotone_depfunction_poset_pair ; intro j ; exact (pr2 (fs j))). - abstract (intros z P f g ; use eq_monotone_function ; intros w ; cbn ; apply poset_enrichment_obj_prod_pair_pr). - abstract (intros z P φ₁ φ₂ q ; use eq_monotone_function ; intro w ; use poset_enrichment_prod_arr_eq ; intro j ; exact (eqtohomot (maponpaths (λ f, pr1 f) (q j)) w)). 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.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.