fact: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions