Proposition bottom_element_eq {X : hSet} (RX : PartialOrder X) (b₁ b₂ : bottom_element RX) : b₁ = b₂. Proof. use subtypePath. { intro. use impred ; intro. apply propproperty. } use (antisymm_PartialOrder RX). - apply b₁. - apply b₂. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.