Proposition transportf_bottom_element {X : hSet} {PX PX' : PartialOrder X} (p : PX = PX') (x : bottom_element PX) : pr1 (transportf bottom_element p x) = pr1 x. Proof. induction p ; cbn. 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.