blob: 756877c95c30074a76180e8e327b8dd0362c5f65 (
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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
|
{-# OPTIONS --without-K --safe #-}
open import Relation.Binary
module Cfe.Language.Properties
{c ℓ} (over : Setoid c ℓ)
where
open Setoid over using () renaming (Carrier to C)
open import Cfe.Language.Base over
-- open Language
open import Data.List
open import Data.List.Relation.Binary.Equality.Setoid over
open import Function
open import Level hiding (Lift)
≈-refl : ∀ {a} → Reflexive (_≈_ {a})
≈-refl {x = A} = record
{ f = id
; f⁻¹ = id
}
≈-sym : ∀ {a b} → Sym (_≈_ {a} {b}) _≈_
≈-sym A≈B = record
{ f = A≈B.f⁻¹
; f⁻¹ = A≈B.f
}
where
module A≈B = _≈_ A≈B
≈-trans : ∀ {a b c} → Trans (_≈_ {a}) (_≈_ {b} {c}) _≈_
≈-trans {i = A} {B} {C} A≈B B≈C = record
{ f = B≈C.f ∘ A≈B.f
; f⁻¹ = A≈B.f⁻¹ ∘ B≈C.f⁻¹
}
where
module A≈B = _≈_ A≈B
module B≈C = _≈_ B≈C
≈-isEquivalence : ∀ {a} → IsEquivalence (_≈_ {a})
≈-isEquivalence = record
{ refl = ≈-refl
; sym = ≈-sym
; trans = ≈-trans
}
setoid : ∀ a → Setoid (c ⊔ ℓ ⊔ suc a) (c ⊔ ℓ ⊔ a)
setoid a = record { isEquivalence = ≈-isEquivalence {a} }
≤-refl : ∀ {a} → Reflexive (_≤_ {a})
≤-refl = record
{ f = id
}
≤-reflexive : ∀ {a b} → _≈_ {a} {b} ⇒ _≤_
≤-reflexive A≈B = record
{ f = A≈B.f
}
where
module A≈B = _≈_ A≈B
≤-trans : ∀ {a b c} → Trans (_≤_ {a}) (_≤_ {b} {c}) _≤_
≤-trans A≤B B≤C = record
{ f = B≤C.f ∘ A≤B.f
}
where
module A≤B = _≤_ A≤B
module B≤C = _≤_ B≤C
≤-antisym : ∀ {a b} → Antisym (_≤_ {a} {b}) _≤_ _≈_
≤-antisym A≤B B≤A = record
{ f = A≤B.f
; f⁻¹ = B≤A.f
}
where
module A≤B = _≤_ A≤B
module B≤A = _≤_ B≤A
≤-min : ∀ {b} → Min (_≤_ {b = b}) ∅
≤-min A = record
{ f = λ ()
}
≤-isPartialOrder : ∀ a → IsPartialOrder (_≈_ {a}) _≤_
≤-isPartialOrder a = record
{ isPreorder = record
{ isEquivalence = ≈-isEquivalence
; reflexive = ≤-reflexive
; trans = ≤-trans
}
; antisym = ≤-antisym
}
poset : ∀ a → Poset (c ⊔ ℓ ⊔ suc a) (c ⊔ ℓ ⊔ a) (c ⊔ a)
poset a = record { isPartialOrder = ≤-isPartialOrder a }
lift-cong : ∀ {a} b (L : Language a) → Lift b L ≈ L
lift-cong b L = record
{ f = lower
; f⁻¹ = lift
}
|
