{-# OPTIONS --without-K #-}
module Data.One where
open import Data.Unit public renaming (⊤ to 𝟙; tt to 0₁)