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