------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the polymorphic unit type
-- Defines Decidable Equality and Decidable Ordering as well
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.Unit.Polymorphic.Properties where
 
open import Level using (Level)
open import Function.Bundles using (_↔_; mk↔)
open import Data.Product.Base using (_,_)
open import Data.Sum.Base using (inj₁)
open import Data.Unit.Base renaming (⊤ to ⊤*)
open import Data.Unit.Polymorphic.Base using (⊤; tt)
open import Relation.Nullary.Decidable using (yes)
open import Relation.Binary.Bundles
  using (Setoid; DecSetoid; Preorder; Poset; TotalOrder; DecTotalOrder)
open import Relation.Binary.Structures
  using (IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder)
open import Relation.Binary.Definitions
  using (DecidableEquality; Antisymmetric; Total)
open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; refl; trans)
open import Relation.Binary.PropositionalEquality.Properties
  using (decSetoid; setoid; isEquivalence)
 
private
  variable
    ℓ : Level
 
------------------------------------------------------------------------
-- Equality
------------------------------------------------------------------------
 
infix  _≟_
 
_≟_ : DecidableEquality (⊤ {ℓ})
_ ≟ _ = 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 ℓ
  }
 
⊤↔⊤* : ⊤ {ℓ} ↔ ⊤*
⊤↔⊤* = mk↔ ((λ _ → refl) , (λ _ → refl))