Proposition dirprod_pr1_is_strict_and_monotone {X₁ X₂ : hSet} (R₁ : pointed_PartialOrder X₁) (R₂ : pointed_PartialOrder X₂) : is_strict_and_monotone (prod_pointed_PartialOrder R₁ R₂) R₁ dirprod_pr1. Proof. split. - apply dirprod_pr1_is_monotone. - apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.