Lemma wosub_univalence_compute {X:hSet} (S T : WOSubset X) (e : S = T) : wosub_univalence S T e = wosub_univalence_map S T e. Proof. reflexivity. 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.