------------------------------------------------------------------------ -- The Agda standard library -- -- The unit type and the total relation on unit ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.Unit.Base where ------------------------------------------------------------------------ -- A unit type defined as a record type -- Note that by default the unit type is not universe polymorphic as it -- often results in unsolved metas. See `Data.Unit.Polymorphic` for a -- universe polymorphic variant. -- Note also that the name of this type is "\top", not T. open import Agda.Builtin.Unit public using (⊤; tt)