1
------------------------------------------------------------------------
2
-- The Agda standard library
4
-- A universe which includes several kinds of "relatedness" for sets,
5
-- such as equivalences, surjections and bijections
6
------------------------------------------------------------------------
8
module Function.Related where
12
open import Function.Equality using (_⟨$⟩_)
13
open import Function.Equivalence as Eq using (Equivalence)
14
open import Function.Injection as Inj using (Injection; _↣_)
15
open import Function.Inverse as Inv using (Inverse; _↔_)
16
open import Function.LeftInverse as LeftInv using (LeftInverse)
17
open import Function.Surjection as Surj using (Surjection)
18
open import Relation.Binary
19
open import Relation.Binary.PropositionalEquality as P using (_≡_)
21
------------------------------------------------------------------------
24
-- Synonyms which are used to make _∼[_]_ below "constructor-headed"
25
-- (which implies that Agda can deduce the universe code from an
26
-- expression matching any of the right-hand sides).
28
record _←_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
34
record _↢_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
40
------------------------------------------------------------------------
43
-- There are several kinds of "relatedness".
45
-- The idea to include kinds other than equivalence and bijection came
46
-- from Simon Thompson and Bengt Nordström. /NAD
49
implication reverse-implication
51
injection reverse-injection
52
left-inverse surjection
56
-- Interpretation of the codes above. The code "bijection" is
57
-- interpreted as Inverse rather than Bijection; the two types are
62
_∼[_]_ : ∀ {ℓ₁ ℓ₂} → Set ℓ₁ → Kind → Set ℓ₂ → Set _
63
A ∼[ implication ] B = A → B
64
A ∼[ reverse-implication ] B = A ← B
65
A ∼[ equivalence ] B = Equivalence (P.setoid A) (P.setoid B)
66
A ∼[ injection ] B = Injection (P.setoid A) (P.setoid B)
67
A ∼[ reverse-injection ] B = A ↢ B
68
A ∼[ left-inverse ] B = LeftInverse (P.setoid A) (P.setoid B)
69
A ∼[ surjection ] B = Surjection (P.setoid A) (P.setoid B)
70
A ∼[ bijection ] B = Inverse (P.setoid A) (P.setoid B)
72
-- A non-infix synonym.
74
Related : Kind → ∀ {ℓ₁ ℓ₂} → Set ℓ₁ → Set ℓ₂ → Set _
75
Related k A B = A ∼[ k ] B
77
-- The bijective equality implies any kind of relatedness.
79
↔⇒ : ∀ {k x y} {X : Set x} {Y : Set y} →
80
X ∼[ bijection ] Y → X ∼[ k ] Y
81
↔⇒ {implication} = _⟨$⟩_ ∘ Inverse.to
82
↔⇒ {reverse-implication} = lam ∘′ _⟨$⟩_ ∘ Inverse.from
83
↔⇒ {equivalence} = Inverse.equivalence
84
↔⇒ {injection} = Inverse.injection
85
↔⇒ {reverse-injection} = lam ∘′ Inverse.injection ∘ Inv.sym
86
↔⇒ {left-inverse} = Inverse.left-inverse
87
↔⇒ {surjection} = Inverse.surjection
90
-- Actual equality also implies any kind of relatedness.
92
≡⇒ : ∀ {k ℓ} {X Y : Set ℓ} → X ≡ Y → X ∼[ k ] Y
95
------------------------------------------------------------------------
96
-- Special kinds of kinds
98
-- Kinds whose interpretation is symmetric.
100
data Symmetric-kind : Set where
101
equivalence bijection : Symmetric-kind
105
⌊_⌋ : Symmetric-kind → Kind
106
⌊ equivalence ⌋ = equivalence
107
⌊ bijection ⌋ = bijection
109
-- The proof of symmetry can be found below.
111
-- Kinds whose interpretation include a function which "goes in the
112
-- forward direction".
114
data Forward-kind : Set where
115
implication equivalence injection
116
left-inverse surjection bijection : Forward-kind
120
⌊_⌋→ : Forward-kind → Kind
121
⌊ implication ⌋→ = implication
122
⌊ equivalence ⌋→ = equivalence
123
⌊ injection ⌋→ = injection
124
⌊ left-inverse ⌋→ = left-inverse
125
⌊ surjection ⌋→ = surjection
126
⌊ bijection ⌋→ = bijection
130
⇒→ : ∀ {k x y} {X : Set x} {Y : Set y} → X ∼[ ⌊ k ⌋→ ] Y → X → Y
131
⇒→ {implication} = id
132
⇒→ {equivalence} = _⟨$⟩_ ∘ Equivalence.to
133
⇒→ {injection} = _⟨$⟩_ ∘ Injection.to
134
⇒→ {left-inverse} = _⟨$⟩_ ∘ LeftInverse.to
135
⇒→ {surjection} = _⟨$⟩_ ∘ Surjection.to
136
⇒→ {bijection} = _⟨$⟩_ ∘ Inverse.to
138
-- Kinds whose interpretation include a function which "goes backwards".
140
data Backward-kind : Set where
141
reverse-implication equivalence reverse-injection
142
left-inverse surjection bijection : Backward-kind
146
⌊_⌋← : Backward-kind → Kind
147
⌊ reverse-implication ⌋← = reverse-implication
148
⌊ equivalence ⌋← = equivalence
149
⌊ reverse-injection ⌋← = reverse-injection
150
⌊ left-inverse ⌋← = left-inverse
151
⌊ surjection ⌋← = surjection
152
⌊ bijection ⌋← = bijection
156
⇒← : ∀ {k x y} {X : Set x} {Y : Set y} → X ∼[ ⌊ k ⌋← ] Y → Y → X
157
⇒← {reverse-implication} = app-←
158
⇒← {equivalence} = _⟨$⟩_ ∘ Equivalence.from
159
⇒← {reverse-injection} = _⟨$⟩_ ∘ Injection.to ∘ app-↢
160
⇒← {left-inverse} = _⟨$⟩_ ∘ LeftInverse.from
161
⇒← {surjection} = _⟨$⟩_ ∘ Surjection.from
162
⇒← {bijection} = _⟨$⟩_ ∘ Inverse.from
164
-- Kinds whose interpretation include functions going in both
167
data Equivalence-kind : Set where
168
equivalence left-inverse surjection bijection : Equivalence-kind
172
⌊_⌋⇔ : Equivalence-kind → Kind
173
⌊ equivalence ⌋⇔ = equivalence
174
⌊ left-inverse ⌋⇔ = left-inverse
175
⌊ surjection ⌋⇔ = surjection
176
⌊ bijection ⌋⇔ = bijection
180
⇒⇔ : ∀ {k x y} {X : Set x} {Y : Set y} →
181
X ∼[ ⌊ k ⌋⇔ ] Y → X ∼[ equivalence ] Y
182
⇒⇔ {equivalence} = id
183
⇒⇔ {left-inverse} = LeftInverse.equivalence
184
⇒⇔ {surjection} = Surjection.equivalence
185
⇒⇔ {bijection} = Inverse.equivalence
187
-- Conversions between special kinds.
189
⇔⌊_⌋ : Symmetric-kind → Equivalence-kind
190
⇔⌊ equivalence ⌋ = equivalence
191
⇔⌊ bijection ⌋ = bijection
193
→⌊_⌋ : Equivalence-kind → Forward-kind
194
→⌊ equivalence ⌋ = equivalence
195
→⌊ left-inverse ⌋ = left-inverse
196
→⌊ surjection ⌋ = surjection
197
→⌊ bijection ⌋ = bijection
199
←⌊_⌋ : Equivalence-kind → Backward-kind
200
←⌊ equivalence ⌋ = equivalence
201
←⌊ left-inverse ⌋ = left-inverse
202
←⌊ surjection ⌋ = surjection
203
←⌊ bijection ⌋ = bijection
205
------------------------------------------------------------------------
208
-- For every kind there is an opposite kind.
211
implication op = reverse-implication
212
reverse-implication op = implication
213
equivalence op = equivalence
214
injection op = reverse-injection
215
reverse-injection op = injection
216
left-inverse op = surjection
217
surjection op = left-inverse
218
bijection op = bijection
220
-- For every morphism there is a corresponding reverse morphism of the
223
reverse : ∀ {k a b} {A : Set a} {B : Set b} →
224
A ∼[ k ] B → B ∼[ k op ] A
225
reverse {implication} = lam
226
reverse {reverse-implication} = app-←
227
reverse {equivalence} = Eq.sym
228
reverse {injection} = lam
229
reverse {reverse-injection} = app-↢
230
reverse {left-inverse} = Surj.fromRightInverse
231
reverse {surjection} = Surjection.right-inverse
232
reverse {bijection} = Inv.sym
234
------------------------------------------------------------------------
235
-- Equational reasoning
237
-- Equational reasoning for related things.
239
module EquationalReasoning where
243
refl : ∀ {k ℓ} → Reflexive (Related k {ℓ})
244
refl {implication} = id
245
refl {reverse-implication} = lam id
246
refl {equivalence} = Eq.id
247
refl {injection} = Inj.id
248
refl {reverse-injection} = lam Inj.id
249
refl {left-inverse} = LeftInv.id
250
refl {surjection} = Surj.id
251
refl {bijection} = Inv.id
253
trans : ∀ {k ℓ₁ ℓ₂ ℓ₃} →
254
Trans (Related k {ℓ₁} {ℓ₂})
255
(Related k {ℓ₂} {ℓ₃})
256
(Related k {ℓ₁} {ℓ₃})
257
trans {implication} = flip _∘′_
258
trans {reverse-implication} = λ f g → lam (app-← f ∘ app-← g)
259
trans {equivalence} = flip Eq._∘_
260
trans {injection} = flip Inj._∘_
261
trans {reverse-injection} = λ f g → lam (Inj._∘_ (app-↢ f) (app-↢ g))
262
trans {left-inverse} = flip LeftInv._∘_
263
trans {surjection} = flip Surj._∘_
264
trans {bijection} = flip Inv._∘_
267
Sym (Related ⌊ k ⌋ {ℓ₁} {ℓ₂})
268
(Related ⌊ k ⌋ {ℓ₂} {ℓ₁})
269
sym {equivalence} = Eq.sym
270
sym {bijection} = Inv.sym
273
infixr 2 _∼⟨_⟩_ _↔⟨_⟩_ _≡⟨_⟩_
275
_∼⟨_⟩_ : ∀ {k x y z} (X : Set x) {Y : Set y} {Z : Set z} →
276
X ∼[ k ] Y → Y ∼[ k ] Z → X ∼[ k ] Z
277
_ ∼⟨ X↝Y ⟩ Y↝Z = trans X↝Y Y↝Z
279
-- Isomorphisms can be combined with any other kind of relatedness.
281
_↔⟨_⟩_ : ∀ {k x y z} (X : Set x) {Y : Set y} {Z : Set z} →
282
X ↔ Y → Y ∼[ k ] Z → X ∼[ k ] Z
283
X ↔⟨ X↔Y ⟩ Y⇔Z = X ∼⟨ ↔⇒ X↔Y ⟩ Y⇔Z
285
_≡⟨_⟩_ : ∀ {k ℓ z} (X : Set ℓ) {Y : Set ℓ} {Z : Set z} →
286
X ≡ Y → Y ∼[ k ] Z → X ∼[ k ] Z
287
X ≡⟨ X≡Y ⟩ Y⇔Z = X ∼⟨ ≡⇒ X≡Y ⟩ Y⇔Z
289
_∎ : ∀ {k x} (X : Set x) → X ∼[ k ] X
292
-- For a symmetric kind and a fixed universe level we can construct a
295
setoid : Symmetric-kind → (ℓ : Level) → Setoid _ _
298
; _≈_ = Related ⌊ k ⌋
300
record {refl = _ ∎; sym = sym; trans = _∼⟨_⟩_ _}
301
} where open EquationalReasoning
303
-- For an arbitrary kind and a fixed universe level we can construct a
306
preorder : Kind → (ℓ : Level) → Preorder _ _ _
307
preorder k ℓ = record
311
; isPreorder = record
312
{ isEquivalence = Setoid.isEquivalence (setoid bijection ℓ)
316
} where open EquationalReasoning
318
------------------------------------------------------------------------
319
-- Some induced relations
321
-- Every unary relation induces a preorder and, for symmetric kinds,
322
-- an equivalence. (No claim is made that these relations are unique.)
324
InducedRelation₁ : Kind → ∀ {a s} {A : Set a} →
325
(A → Set s) → A → A → Set _
326
InducedRelation₁ k S = λ x y → S x ∼[ k ] S y
328
InducedPreorder₁ : Kind → ∀ {a s} {A : Set a} →
329
(A → Set s) → Preorder _ _ _
330
InducedPreorder₁ k S = record
332
; _∼_ = InducedRelation₁ k S
333
; isPreorder = record
334
{ isEquivalence = P.isEquivalence
335
; reflexive = reflexive ∘
336
Setoid.reflexive (setoid bijection _) ∘
340
} where open Preorder (preorder _ _)
342
InducedEquivalence₁ : Symmetric-kind → ∀ {a s} {A : Set a} →
343
(A → Set s) → Setoid _ _
344
InducedEquivalence₁ k S = record
345
{ _≈_ = InducedRelation₁ ⌊ k ⌋ S
346
; isEquivalence = record {refl = refl; sym = sym; trans = trans}
347
} where open Setoid (setoid _ _)
349
-- Every binary relation induces a preorder and, for symmetric kinds,
350
-- an equivalence. (No claim is made that these relations are unique.)
352
InducedRelation₂ : Kind → ∀ {a b s} {A : Set a} {B : Set b} →
353
(A → B → Set s) → B → B → Set _
354
InducedRelation₂ k _S_ = λ x y → ∀ {z} → (z S x) ∼[ k ] (z S y)
356
InducedPreorder₂ : Kind → ∀ {a b s} {A : Set a} {B : Set b} →
357
(A → B → Set s) → Preorder _ _ _
358
InducedPreorder₂ k _S_ = record
360
; _∼_ = InducedRelation₂ k _S_
361
; isPreorder = record
362
{ isEquivalence = P.isEquivalence
363
; reflexive = λ x≡y {z} →
365
Setoid.reflexive (setoid bijection _) $
368
; trans = λ i↝j j↝k → trans i↝j j↝k
370
} where open Preorder (preorder _ _)
372
InducedEquivalence₂ : Symmetric-kind →
373
∀ {a b s} {A : Set a} {B : Set b} →
374
(A → B → Set s) → Setoid _ _
375
InducedEquivalence₂ k _S_ = record
376
{ _≈_ = InducedRelation₂ ⌊ k ⌋ _S_
377
; isEquivalence = record
379
; sym = λ i↝j → sym i↝j
380
; trans = λ i↝j j↝k → trans i↝j j↝k
382
} where open Setoid (setoid _ _)
added
removed
src/Function/Related.agda
