Module `UnivMinim`

module UPairSet : CSet.S with type S.elt = Univ.Level.t * Univ.Level.t: Unordered pairs of universe levels (ie (u,v) = (v,u))

val normalize_context_set : lbound:Univ.Level.t -> UGraph.t -> Univ.ContextSet.t -> UnivSubst.universe_opt_subst -> Univ.LSet.t -> UPairSet.t -> (UnivSubst.universe_opt_subst * Univ.LSet.t) Univ.in_universe_context_set