```------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the polymorphic unit type
-- Defines Decidable Equality and Decidable Ordering as well
------------------------------------------------------------------------

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

module Data.Unit.Polymorphic.Properties where

open import Level
open import Data.Sum.Base using (inj₁)
open import Data.Unit.Polymorphic.Base using (⊤; tt)
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

private
variable
ℓ : Level

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

infix 4 _≟_

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

≡-setoid : ∀ ℓ → Setoid ℓ ℓ
≡-setoid _ = setoid ⊤

≡-decSetoid : ∀ ℓ → DecSetoid ℓ ℓ
≡-decSetoid _ = decSetoid _≟_

------------------------------------------------------------------------
-- Ordering
------------------------------------------------------------------------

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

≡-antisym : Antisymmetric {A = ⊤ {ℓ}} _≡_ _≡_
≡-antisym p _ = p

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

≡-isPreorder : ∀ ℓ → IsPreorder {ℓ} {_} {⊤} _≡_ _≡_
≡-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

≡-preorder : ∀ ℓ → Preorder ℓ ℓ ℓ
≡-preorder ℓ = record
{ isPreorder = ≡-isPreorder ℓ
}

≡-poset : ∀ ℓ → Poset ℓ ℓ ℓ
≡-poset ℓ = record
{ isPartialOrder = ≡-isPartialOrder ℓ
}

≡-totalOrder : ∀ ℓ → TotalOrder ℓ ℓ ℓ
≡-totalOrder ℓ = record
{ isTotalOrder = ≡-isTotalOrder ℓ
}

≡-decTotalOrder : ∀ ℓ → DecTotalOrder ℓ ℓ ℓ
≡-decTotalOrder ℓ = record
{ isDecTotalOrder = ≡-isDecTotalOrder ℓ
}
```