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

module Terra.Data.Unit where
open import Agda.Builtin.Unit public
-- record ⊤ : Set where
--   constructor tt

-- {-# BUILTIN UNIT ⊤ #-}
-- {-# COMPILE GHC ⊤ = data () (()) #-}