Agda UALib ↑

---

{-# OPTIONS --without-K --exact-split --safe #-}

module Unit-Type where

open import Universes public

data 𝟙 {𝓤} : 𝓤 ̇ where
 ⋆ : 𝟙