proposition: 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: Proof. split. - apply dirprod_pr1_is_monotone. - apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions