------------------------------------------------------------------------
-- The Agda standard library
--
-- The unit type, Level-monomorphic version
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.Unit where
 
------------------------------------------------------------------------
-- Re-export contents of base module
 
open import Data.Unit.Base public
 
------------------------------------------------------------------------
-- Re-export query operations
 
open import Data.Unit.Properties public
  using (_≟_)