Definition upto' {X:hSet} {C:WOSubset X} (c:C) : proper_subtypes_set X. Proof. exists (upto c). apply hinhpr. exists (pr1 c). intro n. simpl in n. induction n as [n o]. apply o; clear o. apply (TOeq_to_refl C _ _). now apply subtypePath_prop. 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.