diff --git a/docs/src/lib/sets/Universe.md b/docs/src/lib/sets/Universe.md
index 56fe34d298..fbbc6633e4 100644
--- a/docs/src/lib/sets/Universe.md
+++ b/docs/src/lib/sets/Universe.md
@@ -1,11 +1,16 @@
 ```@meta
-CurrentModule = LazySets
+CurrentModule = LazySets.UniverseModule
 ```
 
 # [Universe](@id def_Universe)
 
 ```@docs
 Universe
+```
+
+## Operations
+
+```@docs
 dim(::Universe)
 ρ(::AbstractVector, ::Universe)
 σ(::AbstractVector, ::Universe)
@@ -25,6 +30,5 @@ translate(::Universe, ::AbstractVector)
 translate!(::Universe, ::AbstractVector)
 permute(::Universe, ::AbstractVector{Int})
 complement(::Universe{N}) where {N}
-polyhedron(::Universe)
 reflect(::Universe)
 ```
diff --git a/src/Initialization/init_Polyhedra.jl b/src/Initialization/init_Polyhedra.jl
index 64feb1aee9..f4236b65bd 100644
--- a/src/Initialization/init_Polyhedra.jl
+++ b/src/Initialization/init_Polyhedra.jl
@@ -40,6 +40,5 @@ end
 eval(load_polyhedra_hpolytope())
 eval(load_polyhedra_hpolyhedron())
 eval(load_polyhedra_vpolytope())
-eval(load_polyhedra_universe())
 eval(load_polyhedra_mesh())
 eval(load_polyhedra_lazyset())
diff --git a/src/LazySets.jl b/src/LazySets.jl
index 856ac757a7..11f7479b95 100644
--- a/src/LazySets.jl
+++ b/src/LazySets.jl
@@ -93,7 +93,8 @@ include("Interfaces/AbstractBallp.jl")
 # =============================
 # Types representing basic sets
 # =============================
-include("Sets/Universe.jl")
+include("Sets/Universe/UniverseModule.jl")
+@reexport using ..UniverseModule: Universe
 
 include("Sets/EmptySet/EmptySetModule.jl")
 @reexport using ..EmptySetModule: EmptySet, ∅, _isdisjoint_emptyset
diff --git a/src/Sets/Universe.jl b/src/Sets/Universe.jl
deleted file mode 100644
index 3c5cdb468c..0000000000
--- a/src/Sets/Universe.jl
+++ /dev/null
@@ -1,468 +0,0 @@
-export Universe
-
-"""
-    Universe{N} <: AbstractPolyhedron{N}
-
-Type that represents the universal set, i.e., the set of all elements.
-
-### Fields
-
-- `dim` -- the ambient dimension of the set
-"""
-struct Universe{N} <: AbstractPolyhedron{N}
-    dim::Int
-end
-
-isoperationtype(::Type{<:Universe}) = false
-
-# default constructor of type Float64
-Universe(dim::Int) = Universe{Float64}(dim)
-
-"""
-    constraints(U::Universe{N}) where {N}
-
-Construct an iterator over the constraints of a universe.
-
-### Input
-
-- `U` -- universe
-
-### Output
-
-The empty iterator, as the universe is unconstrained.
-"""
-function constraints(U::Universe{N}) where {N}
-    return EmptyIterator{Vector{N}}()
-end
-
-"""
-    constraints_list(U::Universe{N}) where {N}
-
-Return the list of constraints defining a universe.
-
-### Input
-
-- `U` -- universe
-
-### Output
-
-The empty list of constraints, as the universe is unconstrained.
-"""
-function constraints_list(U::Universe{N}) where {N}
-    return HalfSpace{N,Vector{N}}[]
-end
-
-"""
-    constrained_dimensions(U::Universe)
-
-Return the indices in which a universe is constrained.
-
-### Input
-
-- `U` -- universe
-
-### Output
-
-The empty vector, as the universe is unconstrained in every dimension.
-"""
-function constrained_dimensions(U::Universe)
-    return Int[]
-end
-
-"""
-    dim(U::Universe)
-
-Return the dimension of a universe.
-
-### Input
-
-- `U` -- universe
-
-### Output
-
-The ambient dimension of a universe.
-"""
-function dim(U::Universe)
-    return U.dim
-end
-
-"""
-    ρ(d::AbstractVector, U::Universe)
-
-Return the support function of a universe.
-
-### Input
-
-- `d` -- direction
-- `U` -- universe
-
-### Output
-
-The support function in the given direction.
-
-### Algorithm
-
-If the direction is all zero, the result is zero.
-Otherwise, the result is `Inf`.
-"""
-function ρ(d::AbstractVector, U::Universe)
-    N = promote_type(eltype(d), eltype(U))
-    return iszero(d) ? zero(N) : N(Inf)
-end
-
-"""
-    σ(d::AbstractVector, U::Universe)
-
-Return the support vector of a universe.
-
-### Input
-
-- `d` -- direction
-- `U` -- universe
-
-### Output
-
-A vector with infinity values, except in dimensions where the direction is zero.
-"""
-function σ(d::AbstractVector, U::Universe)
-    N = promote_type(eltype(d), eltype(U))
-    return [iszero(v) ? v : v > zero(N) ? N(Inf) : N(-Inf) for v in d]
-end
-
-"""
-    ∈(x::AbstractVector, U::Universe)
-
-Check whether a given point is contained in a universe.
-
-### Input
-
-- `x` -- point/vector
-- `U` -- universe
-
-### Output
-
-`true`.
-
-### Examples
-
-```jldoctest
-julia> [1.0, 0.0] ∈ Universe(2)
-true
-```
-"""
-function ∈(x::AbstractVector, U::Universe)
-    @assert length(x) == dim(U) "a $(length(x))-dimensional vector is " *
-                                "incompatible with a $(dim(U))-dimensional set"
-    return true
-end
-
-"""
-    an_element(U::Universe{N}) where {N}
-
-Return some element of a universe.
-
-### Input
-
-- `U` -- universe
-
-### Output
-
-The origin.
-"""
-function an_element(U::Universe{N}) where {N}
-    return zeros(N, dim(U))
-end
-
-"""
-    rand(::Type{Universe}; [N]::Type{<:Real}=Float64, [dim]::Int=2,
-         [rng]::AbstractRNG=GLOBAL_RNG, [seed]::Union{Int, Nothing}=nothing)
-
-Create a universe (note that there is nothing to randomize).
-
-### Input
-
-- `Universe` -- type for dispatch
-- `N`        -- (optional, default: `Float64`) numeric type
-- `dim`      -- (optional, default: 2) dimension
-- `rng`      -- (optional, default: `GLOBAL_RNG`) random number generator
-- `seed`     -- (optional, default: `nothing`) seed for reseeding
-
-### Output
-
-The (only) universe of the given numeric type and dimension.
-"""
-function rand(::Type{Universe};
-              N::Type{<:Real}=Float64,
-              dim::Int=2,
-              rng::AbstractRNG=GLOBAL_RNG,
-              seed::Union{Int,Nothing}=nothing)
-    rng = reseed!(rng, seed)
-    return Universe{N}(dim)
-end
-
-"""
-    isempty(U::Universe)
-
-Check whether a universe is empty.
-
-### Input
-
-- `U` -- universe
-
-### Output
-
-`false`.
-"""
-function isempty(U::Universe)
-    return false
-end
-
-"""
-    isbounded(U::Universe)
-
-Check whether a universe is bounded.
-
-### Input
-
-- `U` -- universe
-
-### Output
-
-`false`.
-"""
-function isbounded(U::Universe)
-    return false
-end
-
-function isboundedtype(::Type{<:Universe})
-    return false
-end
-
-"""
-    isuniversal(U::Universe{N}, [witness]::Bool=false) where {N}
-
-Check whether a universe is universal.
-
-### Input
-
-- `U`       -- universe
-- `witness` -- (optional, default: `false`) compute a witness if activated
-
-### Output
-
-* If `witness` option is deactivated: `true`
-* If `witness` option is activated: `(true, [])`
-"""
-function isuniversal(U::Universe{N}, witness::Bool=false) where {N}
-    return witness ? (true, N[]) : true
-end
-
-"""
-    norm(U::Universe, [p]::Real=Inf)
-
-Return the norm of a universe.
-It is the norm of the enclosing ball (of the given ``p``-norm) of minimal volume
-that is centered in the origin.
-
-### Input
-
-- `U` -- universe
-- `p` -- (optional, default: `Inf`) norm
-
-### Output
-
-An error.
-"""
-function norm(U::Universe, p::Real=Inf)
-    return error("a universe does not have a norm")
-end
-
-"""
-    radius(U::Universe, [p]::Real=Inf)
-
-Return the radius of a universe.
-It is the radius of the enclosing ball (of the given ``p``-norm) of minimal
-volume.
-
-### Input
-
-- `U` -- universe
-- `p` -- (optional, default: `Inf`) norm
-
-### Output
-
-An error.
-"""
-function radius(U::Universe, p::Real=Inf)
-    return error("a universe does not have a radius")
-end
-
-"""
-    diameter(U::Universe, [p]::Real=Inf)
-
-Return the diameter of a universe.
-It is the diameter of the enclosing ball (of the given ``p``-norm) of minimal
-volume .
-
-### Input
-
-- `U` -- universe
-- `p` -- (optional, default: `Inf`) norm
-
-### Output
-
-An error.
-"""
-function diameter(U::Universe, p::Real=Inf)
-    return error("a universe does not have a diameter")
-end
-
-"""
-    translate(U::Universe, v::AbstractVector)
-
-Translate (i.e., shift) a universe by a given vector.
-
-### Input
-
-- `U` -- universe
-- `v` -- translation vector
-
-### Output
-
-The universe.
-"""
-function translate(U::Universe, v::AbstractVector)
-    return translate!(U, v)  # no need to copy
-end
-
-"""
-    translate!(U::Universe, v::AbstractVector)
-
-Translate (i.e., shift) a universe by a given vector, in-place.
-
-### Input
-
-- `U` -- universe
-- `v` -- translation vector
-
-### Output
-
-The universe.
-"""
-function translate!(U::Universe, v::AbstractVector)
-    @assert length(v) == dim(U) "cannot translate a $(dim(U))-dimensional " *
-                                "set by a $(length(v))-dimensional vector"
-    return U
-end
-
-function linear_map_inverse(Minv::AbstractMatrix{N}, U::Universe{N}) where {N}
-    @assert size(Minv, 1) == dim(U) "a linear map of size $(size(Minv)) " *
-                                    "cannot be applied to a universe of dimension $(dim(U))"
-    n = size(Minv, 2)
-    return Universe{N}(n)
-end
-
-function project(U::Universe{N}, block::AbstractVector{Int}; kwargs...) where {N}
-    return Universe{N}(length(block))
-end
-
-"""
-    permute(U::Universe, p::AbstractVector{Int})
-
-Permute the dimensions according to a permutation vector.
-
-### Input
-
-- `U` -- universe
-- `p` -- permutation vector
-
-### Output
-
-The same universe.
-"""
-function permute(U::Universe, p::AbstractVector{Int})
-    return U
-end
-
-function tosimplehrep(U::Universe)
-    return tosimplehrep(constraints_list(U); n=dim(U))
-end
-
-"""
-    complement(U::Universe{N}) where {N}
-
-Return the complement of an universe.
-
-### Input
-
-- `∅` -- universe
-
-### Output
-
-The empty set of the same dimension.
-"""
-function complement(U::Universe{N}) where {N}
-    return EmptySet{N}(dim(U))
-end
-
-function load_polyhedra_universe() # function to be loaded by Requires
-    return quote
-        # see the interface file init_Polyhedra.jl for the imports
-
-        """
-            polyhedron(U::Universe; [backend]=default_polyhedra_backend(P))
-
-        Return an `HRep` polyhedron from `Polyhedra.jl` given a universe.
-
-        ### Input
-
-        - `U`       -- universe
-        - `backend` -- (optional, default: call `default_polyhedra_backend(P)`)
-                       the backend for polyhedral computations
-
-        ### Output
-
-        An `HRep` polyhedron.
-
-        ### Notes
-
-        For further information on the supported backends see
-        [Polyhedra's documentation](https://juliapolyhedra.github.io/).
-        """
-        function polyhedron(U::Universe; backend=default_polyhedra_backend(U))
-            A, b = tosimplehrep(U)
-            return Polyhedra.polyhedron(Polyhedra.hrep(A, b), backend)
-        end
-    end
-end  # quote / load_polyhedra_universe()
-
-"""
-    reflect(U::Universe)
-
-Concrete reflection of a universe `U`, resulting in the reflected set `-U`.
-
-### Input
-
-- `U` -- universe
-
-### Output
-
-The same universe.
-"""
-function reflect(U::Universe)
-    return U
-end
-
-function scale(α::Real, U::Universe{N}) where {N}
-    if iszero(α)
-        return ZeroSet{N}(dim(U))
-    end
-    return U
-end
-
-function scale!(α::Real, U::Universe)
-    if iszero(α)
-        throw(ArgumentError("cannot 0-scale a universe in-place"))
-    end
-    return U
-end
diff --git a/src/Sets/Universe/Universe.jl b/src/Sets/Universe/Universe.jl
new file mode 100644
index 0000000000..14dff147c1
--- /dev/null
+++ b/src/Sets/Universe/Universe.jl
@@ -0,0 +1,15 @@
+"""
+    Universe{N} <: AbstractPolyhedron{N}
+
+Type that represents the universal set, i.e., the set of all elements.
+
+### Fields
+
+- `dim` -- the ambient dimension of the set
+"""
+struct Universe{N} <: AbstractPolyhedron{N}
+    dim::Int
+end
+
+# default constructor of type Float64
+Universe(dim::Int) = Universe{Float64}(dim)
diff --git a/src/Sets/Universe/UniverseModule.jl b/src/Sets/Universe/UniverseModule.jl
new file mode 100644
index 0000000000..df432b6655
--- /dev/null
+++ b/src/Sets/Universe/UniverseModule.jl
@@ -0,0 +1,53 @@
+module UniverseModule
+
+using Reexport, Requires
+
+using ..LazySets: AbstractPolyhedron, HalfSpace, default_polyhedra_backend
+using Random: AbstractRNG, GLOBAL_RNG
+using ReachabilityBase.Distribution: reseed!
+using ReachabilityBase.Iteration: EmptyIterator
+using ReachabilityBase.Require
+
+@reexport import ..API: an_element, complement, constraints, constraints_list,
+                        diameter, dim, isbounded, isboundedtype, isempty,
+                        isoperationtype, isuniversal, norm, radius, rand,
+                        reflect, ∈, permute, project, scale, scale!, ρ, σ,
+                        translate, translate!
+@reexport import ..LazySets: constrained_dimensions, linear_map_inverse,
+                             tosimplehrep
+@reexport using ..API
+
+export Universe
+
+include("Universe.jl")
+
+include("an_element.jl")
+include("complement.jl")
+include("constraints.jl")
+include("constraints_list.jl")
+include("diameter.jl")
+include("dim.jl")
+include("isbounded.jl")
+include("isboundedtype.jl")
+include("isempty.jl")
+include("isoperationtype.jl")
+include("isuniversal.jl")
+include("norm.jl")
+include("radius.jl")
+include("rand.jl")
+include("reflect.jl")
+include("in.jl")
+include("permute.jl")
+include("project.jl")
+include("scale.jl")
+include("support_function.jl")
+include("support_vector.jl")
+include("translate.jl")
+
+include("constrained_dimensions.jl")
+include("linear_map_inverse.jl")
+include("tosimplehrep.jl")
+
+include("init.jl")
+
+end  # module
diff --git a/src/Sets/Universe/an_element.jl b/src/Sets/Universe/an_element.jl
new file mode 100644
index 0000000000..cf19e19675
--- /dev/null
+++ b/src/Sets/Universe/an_element.jl
@@ -0,0 +1,16 @@
+"""
+    an_element(U::Universe{N}) where {N}
+
+Return some element of a universe.
+
+### Input
+
+- `U` -- universe
+
+### Output
+
+The origin.
+"""
+function an_element(U::Universe{N}) where {N}
+    return zeros(N, dim(U))
+end
diff --git a/src/Sets/Universe/complement.jl b/src/Sets/Universe/complement.jl
new file mode 100644
index 0000000000..bd80d56af6
--- /dev/null
+++ b/src/Sets/Universe/complement.jl
@@ -0,0 +1,18 @@
+"""
+    complement(U::Universe{N}) where {N}
+
+Return the complement of an universe.
+
+### Input
+
+- `∅` -- universe
+
+### Output
+
+The empty set of the same dimension.
+"""
+function complement(U::Universe{N}) where {N}
+    require(@__MODULE__, :LazySets; fun_name="complement")
+
+    return EmptySet{N}(dim(U))
+end
diff --git a/src/Sets/Universe/constrained_dimensions.jl b/src/Sets/Universe/constrained_dimensions.jl
new file mode 100644
index 0000000000..27c61cc280
--- /dev/null
+++ b/src/Sets/Universe/constrained_dimensions.jl
@@ -0,0 +1,16 @@
+"""
+    constrained_dimensions(U::Universe)
+
+Return the indices in which a universe is constrained.
+
+### Input
+
+- `U` -- universe
+
+### Output
+
+The empty vector, as the universe is unconstrained in every dimension.
+"""
+function constrained_dimensions(U::Universe)
+    return Int[]
+end
diff --git a/src/Sets/Universe/constraints.jl b/src/Sets/Universe/constraints.jl
new file mode 100644
index 0000000000..2a9400b46b
--- /dev/null
+++ b/src/Sets/Universe/constraints.jl
@@ -0,0 +1,16 @@
+"""
+    constraints(U::Universe{N}) where {N}
+
+Construct an iterator over the constraints of a universe.
+
+### Input
+
+- `U` -- universe
+
+### Output
+
+The empty iterator, as the universe is unconstrained.
+"""
+function constraints(U::Universe{N}) where {N}
+    return EmptyIterator{Vector{N}}()
+end
diff --git a/src/Sets/Universe/constraints_list.jl b/src/Sets/Universe/constraints_list.jl
new file mode 100644
index 0000000000..820f1b6cbc
--- /dev/null
+++ b/src/Sets/Universe/constraints_list.jl
@@ -0,0 +1,16 @@
+"""
+    constraints_list(U::Universe{N}) where {N}
+
+Return the list of constraints defining a universe.
+
+### Input
+
+- `U` -- universe
+
+### Output
+
+The empty list of constraints, as the universe is unconstrained.
+"""
+function constraints_list(U::Universe{N}) where {N}
+    return HalfSpace{N,Vector{N}}[]
+end
diff --git a/src/Sets/Universe/diameter.jl b/src/Sets/Universe/diameter.jl
new file mode 100644
index 0000000000..bc5ba13da7
--- /dev/null
+++ b/src/Sets/Universe/diameter.jl
@@ -0,0 +1,19 @@
+"""
+    diameter(U::Universe, [p]::Real=Inf)
+
+Return the diameter of a universe.
+It is the diameter of the enclosing ball (of the given ``p``-norm) of minimal
+volume .
+
+### Input
+
+- `U` -- universe
+- `p` -- (optional, default: `Inf`) norm
+
+### Output
+
+An error.
+"""
+function diameter(U::Universe, p::Real=Inf)
+    return error("a universe does not have a diameter")
+end
diff --git a/src/Sets/Universe/dim.jl b/src/Sets/Universe/dim.jl
new file mode 100644
index 0000000000..76d44da48f
--- /dev/null
+++ b/src/Sets/Universe/dim.jl
@@ -0,0 +1,16 @@
+"""
+    dim(U::Universe)
+
+Return the dimension of a universe.
+
+### Input
+
+- `U` -- universe
+
+### Output
+
+The ambient dimension of a universe.
+"""
+function dim(U::Universe)
+    return U.dim
+end
diff --git a/src/Sets/Universe/in.jl b/src/Sets/Universe/in.jl
new file mode 100644
index 0000000000..7eee305583
--- /dev/null
+++ b/src/Sets/Universe/in.jl
@@ -0,0 +1,26 @@
+"""
+    ∈(x::AbstractVector, U::Universe)
+
+Check whether a given point is contained in a universe.
+
+### Input
+
+- `x` -- point/vector
+- `U` -- universe
+
+### Output
+
+`true`.
+
+### Examples
+
+```jldoctest
+julia> [1.0, 0.0] ∈ Universe(2)
+true
+```
+"""
+function ∈(x::AbstractVector, U::Universe)
+    @assert length(x) == dim(U) "a $(length(x))-dimensional vector is " *
+                                "incompatible with a $(dim(U))-dimensional set"
+    return true
+end
diff --git a/src/Sets/Universe/init.jl b/src/Sets/Universe/init.jl
new file mode 100644
index 0000000000..ddd845644b
--- /dev/null
+++ b/src/Sets/Universe/init.jl
@@ -0,0 +1,3 @@
+function __init__()
+    @require LazySets = "b4f0291d-fe17-52bc-9479-3d1a343d9043" include("init_LazySets.jl")
+end
diff --git a/src/Sets/Universe/init_LazySets.jl b/src/Sets/Universe/init_LazySets.jl
new file mode 100644
index 0000000000..e85bf07ec1
--- /dev/null
+++ b/src/Sets/Universe/init_LazySets.jl
@@ -0,0 +1,2 @@
+using .LazySets.EmptySetModule: EmptySet
+using .LazySets.ZeroSetModule: ZeroSet
diff --git a/src/Sets/Universe/isbounded.jl b/src/Sets/Universe/isbounded.jl
new file mode 100644
index 0000000000..c509f89367
--- /dev/null
+++ b/src/Sets/Universe/isbounded.jl
@@ -0,0 +1,16 @@
+"""
+    isbounded(U::Universe)
+
+Check whether a universe is bounded.
+
+### Input
+
+- `U` -- universe
+
+### Output
+
+`false`.
+"""
+function isbounded(U::Universe)
+    return false
+end
diff --git a/src/Sets/Universe/isboundedtype.jl b/src/Sets/Universe/isboundedtype.jl
new file mode 100644
index 0000000000..7f7180d7cd
--- /dev/null
+++ b/src/Sets/Universe/isboundedtype.jl
@@ -0,0 +1,3 @@
+function isboundedtype(::Type{<:Universe})
+    return false
+end
diff --git a/src/Sets/Universe/isempty.jl b/src/Sets/Universe/isempty.jl
new file mode 100644
index 0000000000..4666934e51
--- /dev/null
+++ b/src/Sets/Universe/isempty.jl
@@ -0,0 +1,16 @@
+"""
+    isempty(U::Universe)
+
+Check whether a universe is empty.
+
+### Input
+
+- `U` -- universe
+
+### Output
+
+`false`.
+"""
+function isempty(U::Universe)
+    return false
+end
diff --git a/src/Sets/Universe/isoperationtype.jl b/src/Sets/Universe/isoperationtype.jl
new file mode 100644
index 0000000000..cd6b3eeba2
--- /dev/null
+++ b/src/Sets/Universe/isoperationtype.jl
@@ -0,0 +1 @@
+isoperationtype(::Type{<:Universe}) = false
diff --git a/src/Sets/Universe/isuniversal.jl b/src/Sets/Universe/isuniversal.jl
new file mode 100644
index 0000000000..d6cb1217ed
--- /dev/null
+++ b/src/Sets/Universe/isuniversal.jl
@@ -0,0 +1,18 @@
+"""
+    isuniversal(U::Universe{N}, [witness]::Bool=false) where {N}
+
+Check whether a universe is universal.
+
+### Input
+
+- `U`       -- universe
+- `witness` -- (optional, default: `false`) compute a witness if activated
+
+### Output
+
+* If `witness` option is deactivated: `true`
+* If `witness` option is activated: `(true, [])`
+"""
+function isuniversal(U::Universe{N}, witness::Bool=false) where {N}
+    return witness ? (true, N[]) : true
+end
diff --git a/src/Sets/Universe/linear_map_inverse.jl b/src/Sets/Universe/linear_map_inverse.jl
new file mode 100644
index 0000000000..85db68f929
--- /dev/null
+++ b/src/Sets/Universe/linear_map_inverse.jl
@@ -0,0 +1,6 @@
+function linear_map_inverse(Minv::AbstractMatrix{N}, U::Universe{N}) where {N}
+    @assert size(Minv, 1) == dim(U) "a linear map of size $(size(Minv)) " *
+                                    "cannot be applied to a universe of dimension $(dim(U))"
+    n = size(Minv, 2)
+    return Universe{N}(n)
+end
diff --git a/src/Sets/Universe/norm.jl b/src/Sets/Universe/norm.jl
new file mode 100644
index 0000000000..29befc57d8
--- /dev/null
+++ b/src/Sets/Universe/norm.jl
@@ -0,0 +1,19 @@
+"""
+    norm(U::Universe, [p]::Real=Inf)
+
+Return the norm of a universe.
+It is the norm of the enclosing ball (of the given ``p``-norm) of minimal volume
+that is centered in the origin.
+
+### Input
+
+- `U` -- universe
+- `p` -- (optional, default: `Inf`) norm
+
+### Output
+
+An error.
+"""
+function norm(U::Universe, p::Real=Inf)
+    return error("a universe does not have a norm")
+end
diff --git a/src/Sets/Universe/permute.jl b/src/Sets/Universe/permute.jl
new file mode 100644
index 0000000000..b0939c0b9c
--- /dev/null
+++ b/src/Sets/Universe/permute.jl
@@ -0,0 +1,17 @@
+"""
+    permute(U::Universe, p::AbstractVector{Int})
+
+Permute the dimensions according to a permutation vector.
+
+### Input
+
+- `U` -- universe
+- `p` -- permutation vector
+
+### Output
+
+The same universe.
+"""
+function permute(U::Universe, p::AbstractVector{Int})
+    return U
+end
diff --git a/src/Sets/Universe/project.jl b/src/Sets/Universe/project.jl
new file mode 100644
index 0000000000..8ae5d246ff
--- /dev/null
+++ b/src/Sets/Universe/project.jl
@@ -0,0 +1,3 @@
+function project(U::Universe{N}, block::AbstractVector{Int}; kwargs...) where {N}
+    return Universe{N}(length(block))
+end
diff --git a/src/Sets/Universe/radius.jl b/src/Sets/Universe/radius.jl
new file mode 100644
index 0000000000..5004ff7f23
--- /dev/null
+++ b/src/Sets/Universe/radius.jl
@@ -0,0 +1,19 @@
+"""
+    radius(U::Universe, [p]::Real=Inf)
+
+Return the radius of a universe.
+It is the radius of the enclosing ball (of the given ``p``-norm) of minimal
+volume.
+
+### Input
+
+- `U` -- universe
+- `p` -- (optional, default: `Inf`) norm
+
+### Output
+
+An error.
+"""
+function radius(U::Universe, p::Real=Inf)
+    return error("a universe does not have a radius")
+end
diff --git a/src/Sets/Universe/rand.jl b/src/Sets/Universe/rand.jl
new file mode 100644
index 0000000000..6e827ba8d0
--- /dev/null
+++ b/src/Sets/Universe/rand.jl
@@ -0,0 +1,26 @@
+"""
+    rand(::Type{Universe}; [N]::Type{<:Real}=Float64, [dim]::Int=2,
+         [rng]::AbstractRNG=GLOBAL_RNG, [seed]::Union{Int, Nothing}=nothing)
+
+Create a universe (note that there is nothing to randomize).
+
+### Input
+
+- `Universe` -- type for dispatch
+- `N`        -- (optional, default: `Float64`) numeric type
+- `dim`      -- (optional, default: 2) dimension
+- `rng`      -- (optional, default: `GLOBAL_RNG`) random number generator
+- `seed`     -- (optional, default: `nothing`) seed for reseeding
+
+### Output
+
+The (only) universe of the given numeric type and dimension.
+"""
+function rand(::Type{Universe};
+              N::Type{<:Real}=Float64,
+              dim::Int=2,
+              rng::AbstractRNG=GLOBAL_RNG,
+              seed::Union{Int,Nothing}=nothing)
+    rng = reseed!(rng, seed)
+    return Universe{N}(dim)
+end
diff --git a/src/Sets/Universe/reflect.jl b/src/Sets/Universe/reflect.jl
new file mode 100644
index 0000000000..0c095fb607
--- /dev/null
+++ b/src/Sets/Universe/reflect.jl
@@ -0,0 +1,16 @@
+"""
+    reflect(U::Universe)
+
+Concrete reflection of a universe `U`, resulting in the reflected set `-U`.
+
+### Input
+
+- `U` -- universe
+
+### Output
+
+The same universe.
+"""
+function reflect(U::Universe)
+    return U
+end
diff --git a/src/Sets/Universe/scale.jl b/src/Sets/Universe/scale.jl
new file mode 100644
index 0000000000..1ec3c99672
--- /dev/null
+++ b/src/Sets/Universe/scale.jl
@@ -0,0 +1,15 @@
+function scale(α::Real, U::Universe{N}) where {N}
+    if iszero(α)
+        require(@__MODULE__, :LazySets; fun_name="scale")
+
+        return ZeroSet{N}(dim(U))
+    end
+    return U
+end
+
+function scale!(α::Real, U::Universe)
+    if iszero(α)
+        throw(ArgumentError("cannot 0-scale a universe in-place"))
+    end
+    return U
+end
diff --git a/src/Sets/Universe/support_function.jl b/src/Sets/Universe/support_function.jl
new file mode 100644
index 0000000000..2fd2a9d70e
--- /dev/null
+++ b/src/Sets/Universe/support_function.jl
@@ -0,0 +1,23 @@
+"""
+    ρ(d::AbstractVector, U::Universe)
+
+Return the support function of a universe.
+
+### Input
+
+- `d` -- direction
+- `U` -- universe
+
+### Output
+
+The support function in the given direction.
+
+### Algorithm
+
+If the direction is all zero, the result is zero.
+Otherwise, the result is `Inf`.
+"""
+function ρ(d::AbstractVector, U::Universe)
+    N = promote_type(eltype(d), eltype(U))
+    return iszero(d) ? zero(N) : N(Inf)
+end
diff --git a/src/Sets/Universe/support_vector.jl b/src/Sets/Universe/support_vector.jl
new file mode 100644
index 0000000000..6ac6d8a963
--- /dev/null
+++ b/src/Sets/Universe/support_vector.jl
@@ -0,0 +1,18 @@
+"""
+    σ(d::AbstractVector, U::Universe)
+
+Return the support vector of a universe.
+
+### Input
+
+- `d` -- direction
+- `U` -- universe
+
+### Output
+
+A vector with infinity values, except in dimensions where the direction is zero.
+"""
+function σ(d::AbstractVector, U::Universe)
+    N = promote_type(eltype(d), eltype(U))
+    return [iszero(v) ? v : v > zero(N) ? N(Inf) : N(-Inf) for v in d]
+end
diff --git a/src/Sets/Universe/tosimplehrep.jl b/src/Sets/Universe/tosimplehrep.jl
new file mode 100644
index 0000000000..298c5f7c74
--- /dev/null
+++ b/src/Sets/Universe/tosimplehrep.jl
@@ -0,0 +1,3 @@
+function tosimplehrep(U::Universe)
+    return tosimplehrep(constraints_list(U); n=dim(U))
+end
diff --git a/src/Sets/Universe/translate.jl b/src/Sets/Universe/translate.jl
new file mode 100644
index 0000000000..0a9873f5a2
--- /dev/null
+++ b/src/Sets/Universe/translate.jl
@@ -0,0 +1,37 @@
+"""
+    translate(U::Universe, v::AbstractVector)
+
+Translate (i.e., shift) a universe by a given vector.
+
+### Input
+
+- `U` -- universe
+- `v` -- translation vector
+
+### Output
+
+The universe.
+"""
+function translate(U::Universe, v::AbstractVector)
+    return translate!(U, v)  # no need to copy
+end
+
+"""
+    translate!(U::Universe, v::AbstractVector)
+
+Translate (i.e., shift) a universe by a given vector, in-place.
+
+### Input
+
+- `U` -- universe
+- `v` -- translation vector
+
+### Output
+
+The universe.
+"""
+function translate!(U::Universe, v::AbstractVector)
+    @assert length(v) == dim(U) "cannot translate a $(dim(U))-dimensional " *
+                                "set by a $(length(v))-dimensional vector"
+    return U
+end
diff --git a/test/Sets/Universe.jl b/test/Sets/Universe.jl
index 6698eb8dd6..067d0e00d4 100644
--- a/test/Sets/Universe.jl
+++ b/test/Sets/Universe.jl
@@ -55,6 +55,13 @@ for N in [Float64, Rational{Int}, Float32]
     # an_element
     @test an_element(U) ∈ U
 
+    # constrained_dimensions
+    @test constrained_dimensions(U) == Int[]
+
+    # traits
+    @test !isboundedtype(Universe)
+    @test !isoperationtype(Universe)
+
     # norm/radius/diameter functions
     @test_throws ErrorException norm(U)
     @test_throws ErrorException radius(U)
@@ -64,8 +71,10 @@ for N in [Float64, Rational{Int}, Float32]
     @test translate(U, N[1, 2]) == U
     @test translate!(U, N[1, 2]) == U
 
-    # constraints / constraints_list
+    # constraints / constraints_list / tosimplehrep
     @test collect(constraints(U)) == constraints_list(U) == Vector{N}()
+    A, b = tosimplehrep(U)
+    @test A == zeros(N, 0, 2) && b == N[]
 
     # concrete intersection
     @test intersection(B, U) == intersection(U, B) == B