\begin{code}

{-# OPTIONS --without-K --exact-split --safe --no-sized-types --no-guardedness --auto-inline #-}

module MLTT.Empty-Type where

open import MLTT.Universes public

data 𝟘 {𝓤} : 𝓤 ̇ where

\end{code}