------------------------------------------------------------------------ -- 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 }