Definition wosub_univalence_map {X:hSet} (S T : WOSubset X) : (S = T) -> (S ≣ T). Proof. intros e. induction e. unfold wosub_equal. simple refine ((λ L, make_dirprod L L) _). use tpair. + intros x s. assumption. + split. * intros s s' le. assumption. * intros s t Ss St le. assumption. 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.