```------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the unit type
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

-- Disabled to prevent warnings from deprecation warnings for _≤_
{-# OPTIONS --warn=noUserWarning #-}

module Data.Unit.Properties where

open import Data.Sum.Base
open import Data.Unit.Base
open import Level using (0ℓ)
open import Relation.Nullary
open import Relation.Binary hiding (Irrelevant)
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Irrelevancy

⊤-irrelevant : Irrelevant ⊤
⊤-irrelevant _ _ = refl

------------------------------------------------------------------------
-- Equality

infix 4 _≟_

_≟_ : Decidable {A = ⊤} _≡_
_ ≟ _ = yes refl

≡-setoid : Setoid 0ℓ 0ℓ
≡-setoid = setoid ⊤

≡-decSetoid : DecSetoid 0ℓ 0ℓ
≡-decSetoid = decSetoid _≟_

------------------------------------------------------------------------
-- Relational properties

≡-total : Total {A = ⊤} _≡_
≡-total _ _ = inj₁ refl

≡-antisym : Antisymmetric {A = ⊤} _≡_ _≡_
≡-antisym eq _ = eq

------------------------------------------------------------------------
-- Structures

≡-isPreorder : IsPreorder {A = ⊤} _≡_ _≡_
≡-isPreorder = record
{ isEquivalence = isEquivalence
; reflexive     = λ x → x
; trans         = trans
}

≡-isPartialOrder : IsPartialOrder _≡_ _≡_
≡-isPartialOrder = record
{ isPreorder = ≡-isPreorder
; antisym    = ≡-antisym
}

≡-isTotalOrder : IsTotalOrder _≡_ _≡_
≡-isTotalOrder = record
{ isPartialOrder = ≡-isPartialOrder
; total          = ≡-total
}

≡-isDecTotalOrder : IsDecTotalOrder _≡_ _≡_
≡-isDecTotalOrder = record
{ isTotalOrder = ≡-isTotalOrder
; _≟_          = _≟_
; _≤?_         = _≟_
}

------------------------------------------------------------------------
-- Bundles

≡-poset : Poset 0ℓ 0ℓ 0ℓ
≡-poset = record
{ isPartialOrder = ≡-isPartialOrder
}

≡-decTotalOrder : DecTotalOrder 0ℓ 0ℓ 0ℓ
≡-decTotalOrder = record
{ isDecTotalOrder = ≡-isDecTotalOrder
}

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.2

≤-reflexive : _≡_ ⇒ _≤_
≤-reflexive _ = _
{-# WARNING_ON_USAGE ≤-reflexive
"Warning: ≤-reflexive was deprecated in v1.2.
#-}
≤-trans : Transitive _≤_
≤-trans _ _ = _
{-# WARNING_ON_USAGE ≤-trans
"Warning: ≤-trans was deprecated in v1.2.
#-}
≤-antisym : Antisymmetric _≡_ _≤_
≤-antisym  _ _ = refl
{-# WARNING_ON_USAGE ≤-antisym
"Warning: ≤-antisym was deprecated in v1.2.
#-}
≤-total : Total _≤_
≤-total _ _ = inj₁ _
{-# WARNING_ON_USAGE ≤-total
"Warning: ≤-total was deprecated in v1.2.
#-}
infix 4 _≤?_
_≤?_ : Decidable _≤_
_ ≤? _ = yes _
{-# WARNING_ON_USAGE _≤?_
"Warning: _≤?_ was deprecated in v1.2.
#-}
≤-isPreorder : IsPreorder _≡_ _≤_
≤-isPreorder = record
{ isEquivalence = isEquivalence
; reflexive     = ≤-reflexive
; trans         = ≤-trans
}
{-# WARNING_ON_USAGE ≤-isPreorder
"Warning: ≤-isPreorder was deprecated in v1.2.
#-}
≤-isPartialOrder : IsPartialOrder _≡_ _≤_
≤-isPartialOrder = record
{ isPreorder = ≤-isPreorder
; antisym    = ≤-antisym
}
{-# WARNING_ON_USAGE ≤-isPartialOrder
"Warning: ≤-isPartialOrder was deprecated in v1.2.
#-}
≤-isTotalOrder : IsTotalOrder _≡_ _≤_
≤-isTotalOrder = record
{ isPartialOrder = ≤-isPartialOrder
; total          = ≤-total
}
{-# WARNING_ON_USAGE ≤-isTotalOrder
"Warning: ≤-isTotalOrder was deprecated in v1.2.
#-}
≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
≤-isDecTotalOrder = record
{ isTotalOrder = ≤-isTotalOrder
; _≟_          = _≟_
; _≤?_         = _≤?_
}
{-# WARNING_ON_USAGE ≤-isDecTotalOrder
"Warning: ≤-isDecTotalOrder was deprecated in v1.2.
#-}

-- Bundles

≤-poset : Poset 0ℓ 0ℓ 0ℓ
≤-poset = record
{ isPartialOrder = ≤-isPartialOrder
}
{-# WARNING_ON_USAGE ≤-poset
"Warning: ≤-poset was deprecated in v1.2.