Proposition lift_strict_and_monotone_map {X Y : hSet} {f : X → Y} {PX : PartialOrder X} {PY : PartialOrder Y} (Pf : is_monotone PX PY f) : is_strict_and_monotone (lift_pointed_PartialOrder PX) (lift_pointed_PartialOrder PY) (coprodf1 f). Proof. split. - intros [ x | [] ] [ y | [] ] p ; cbn in *. + apply Pf. exact p. + exact p. + exact p. + exact p. - cbn. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets.