Definition TOeq_to_refl_1 {X:hSet} (S : TOSubset X) : ∀ s t : carrier_subset S, pr1 s = pr1 t ⇒ s ≤ t. Proof. intros s t e. induction (subtypePath_prop e). apply TOrefl. Defined.
Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.OrderTheory.OrderedSets.OrderedSets.