------------------------------------------------------------------------
-- 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 4 _≟_

_≟_ : 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))