[Agda] Re: Decidable partial orders

[Peter Berry]

On 25 February 2010 17:19, Peter Berry <pwberry at gmail.com> wrote:
> See the attachment.

Doh. Gmail doesn't realise an .agda file is text. Here it is again.

-----

{-# OPTIONS --universe-polymorphism #-}
module DecPartialOrder where

open import Level
open import Relation.Binary

record IsDecPartialOrder {a ℓ₁ ℓ₂} {A : Set a}
                         (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) :
                         Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  infix 4 _≟_ _≤?_
  field
    isPartialOrder : IsPartialOrder _≈_ _≤_
    _≟_            : Decidable _≈_
    _≤?_           : Decidable _≤_

  private
    module PO = IsPartialOrder isPartialOrder
  open PO public hiding (module Eq)

  module Eq where

    isDecEquivalence : IsDecEquivalence _≈_
    isDecEquivalence = record
      { isEquivalence = PO.isEquivalence
      ; _≟_           = _≟_
      }

    open IsDecEquivalence isDecEquivalence public

record DecPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _≤_
  field
    Carrier           : Set c
    _≈_               : Rel Carrier ℓ₁
    _≤_               : Rel Carrier ℓ₂
    isDecPartialOrder : IsDecPartialOrder _≈_ _≤_


-- 
Peter Berry <pwberry at gmail.com>
Please avoid sending me Word or PowerPoint attachments.
See http://www.gnu.org/philosophy/no-word-attachments.html