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:UGraph.Bound.t -> UGraph.t -> Univ.ContextSet.t -> UnivSubst.universe_opt_subst -> Univ.Level.Set.t -> UPairSet.t -> (UnivSubst.universe_opt_subst * Univ.Level.Set.t) Univ.in_universe_context_set