blob: 04e052ff2dbce90666d411dea3304353aca7bd1e (
plain)
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
80
81
82
83
|
{-# OPTIONS --without-K --safe #-}
open import Level using (Level; _⊔_; suc)
module Preorder.Primitive where
import Relation.Binary.Bundles as SetoidBased using (Preorder)
open import Relation.Binary using (Rel; Reflexive; Symmetric; Transitive; IsEquivalence)
-- A primitive preorder is a type with a reflexive and transitive
-- relation (in other words, a preorder). The "primitive" qualifier
-- is used to distinguish it from preorders in the Agda standard library,
-- which include an underlying equivalence relation on the carrier set.
record Preorder (c ℓ : Level) : Set (suc (c ⊔ ℓ)) where
field
Carrier : Set c
_≲_ : Rel Carrier ℓ
refl : Reflexive _≲_
trans : Transitive _≲_
infix 4 _≲_
-- Isomorphism in a primitive preorder
module Isomorphism {c ℓ : Level} (P : Preorder c ℓ) where
open Preorder P
record _≅_ (x y : Carrier) : Set ℓ where
field
from : x ≲ y
to : y ≲ x
infix 4 _≅_
private
≅-refl : Reflexive _≅_
≅-refl = record
{ from = refl
; to = refl
}
≅-sym : Symmetric _≅_
≅-sym x≅y = let open _≅_ x≅y in record
{ from = to
; to = from
}
≅-trans : Transitive _≅_
≅-trans x≅y y≅z = let open _≅_ in record
{ from = trans (from x≅y) (from y≅z)
; to = trans (to y≅z) (to x≅y)
}
≅-isEquivalence : IsEquivalence _≅_
≅-isEquivalence = record
{ refl = ≅-refl
; sym = ≅-sym
; trans = ≅-trans
}
module ≅ = IsEquivalence ≅-isEquivalence
-- Every primitive preorder can be extended to a setoid-based preorder
-- using isomorphism (_≅_) as the underlying equivalence relation.
setoidBased : {c ℓ : Level} → Preorder c ℓ → SetoidBased.Preorder c ℓ ℓ
setoidBased P = record
{ Carrier = Carrier
; _≈_ = _≅_
; _≲_ = _≲_
; isPreorder = record
{ isEquivalence = ≅-isEquivalence
; reflexive = _≅_.from
; trans = trans
}
}
where
open Preorder P
open Isomorphism P
|
