Lemma upto_eqn {X:hSet} {S T:WOSubset X} (x:X) (Sx : S x) (Tx : T x) : S ≼ T -> upto (x,,Sx) = upto (x,,Tx). Proof. intros ST. apply (invmap (hsubtype_univalence _ _)). intros y. split. - intros [Sy lt]. exists (pr1 ST y Sy). generalize lt; clear lt. apply negf. intros le'. apply (pr2 (wosub_fidelity ST (x,, Sx) (y,, Sy))). now apply (h1'' (S := T) le'). - intros [Ty lt]. assert (Q := wosub_le_subi ST x y Sx Ty); simpl in Q. assert (e : pr1 ST x Sx = Tx). { apply propproperty. } induction e. assert (Sy := Q (wo_lt_to_le _ _ lt) : S y); clear Q. exists Sy. generalize lt; clear lt. apply negf. intros le'. now apply (h1'' (wosub_le_comp ST _ _ le')). 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.