proposition: 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: Proof. reflexivity. Defined.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets