Definition strict_function_on_point {X Y : hSet} {RX : pointed_PartialOrder X} {RY : pointed_PartialOrder Y} {f : X → Y} (Hf : is_strict_and_monotone RX RY f) : f ⊥_{RX} = ⊥_{RY} := pr2 Hf.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.