Source code on Github
------------------------------------------------------------------------
-- The Agda standard library
--
-- A universe polymorphic unit type, as a Lift of the Level 0 one.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Unit.Polymorphic.Base where

open import Level
import Data.Unit.Base as 

------------------------------------------------------------------------
-- A unit type defined as a synonym

 : { : Level}  Set 
 {} = Lift  ⊤.⊤

tt : { : Level}   {}
tt = lift ⊤.tt