/usr/share/agda-stdlib/Data/Unit.agda is in agda-stdlib 0.6-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Some unit types
------------------------------------------------------------------------
module Data.Unit where
open import Data.Sum
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq
using (_≡_; refl)
-- Some types and operations are defined in Data.Unit.Core.
open import Data.Unit.Core public
------------------------------------------------------------------------
-- A unit type defined as a record type
-- Note that the name of this type is "\top", not T.
record ⊤ : Set where
constructor tt
record _≤_ (x y : ⊤) : Set where
------------------------------------------------------------------------
-- Operations
_≟_ : Decidable {A = ⊤} _≡_
_ ≟ _ = yes refl
_≤?_ : Decidable _≤_
_ ≤? _ = yes _
total : Total _≤_
total _ _ = inj₁ _
------------------------------------------------------------------------
-- Properties
preorder : Preorder _ _ _
preorder = PropEq.preorder ⊤
setoid : Setoid _ _
setoid = PropEq.setoid ⊤
decTotalOrder : DecTotalOrder _ _ _
decTotalOrder = record
{ Carrier = ⊤
; _≈_ = _≡_
; _≤_ = _≤_
; isDecTotalOrder = record
{ isTotalOrder = record
{ isPartialOrder = record
{ isPreorder = record
{ isEquivalence = PropEq.isEquivalence
; reflexive = λ _ → _
; trans = λ _ _ → _
}
; antisym = antisym
}
; total = total
}
; _≟_ = _≟_
; _≤?_ = _≤?_
}
}
where
antisym : Antisymmetric _≡_ _≤_
antisym _ _ = refl
decSetoid : DecSetoid _ _
decSetoid = DecTotalOrder.Eq.decSetoid decTotalOrder
poset : Poset _ _ _
poset = DecTotalOrder.poset decTotalOrder
|