1
------------------------------------------------------------------------
3
------------------------------------------------------------------------
5
{-# OPTIONS --universe-polymorphism #-}
7
module Function.Inverse where
10
open import Function as Fun using (flip)
11
open import Function.Bijection hiding (id; _∘_)
12
open import Function.Equality as F
13
using (_⟶_) renaming (_∘_ to _⟪∘⟫_)
14
open import Function.Equivalence as Eq using (Equivalent; ⇔-setoid)
15
open import Function.LeftInverse as Left hiding (id; _∘_)
16
open import Function.Surjection as Surj hiding (id; _∘_)
17
open import Relation.Binary
18
import Relation.Binary.PropositionalEquality as P
22
record _InverseOf_ {f₁ f₂ t₁ t₂}
23
{From : Setoid f₁ f₂} {To : Setoid t₁ t₂}
24
(from : To ⟶ From) (to : From ⟶ To) :
25
Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
27
left-inverse-of : from LeftInverseOf to
28
right-inverse-of : from RightInverseOf to
30
-- The set of all inverses between two setoids.
32
record Inverse {f₁ f₂ t₁ t₂}
33
(From : Setoid f₁ f₂) (To : Setoid t₁ t₂) :
34
Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
38
inverse-of : from InverseOf to
40
open _InverseOf_ inverse-of public
42
left-inverse : LeftInverse From To
46
; left-inverse-of = left-inverse-of
49
open LeftInverse left-inverse public
50
using (injective; injection)
52
bijection : Bijection From To
56
{ injective = injective
59
; right-inverse-of = right-inverse-of
64
open Bijection bijection public
65
using (equivalent; surjective; surjection; right-inverse)
67
-- The set of all inverses between two sets.
71
_⇿_ : ∀ {f t} → Set f → Set t → Set _
72
From ⇿ To = Inverse (P.setoid From) (P.setoid To)
74
-- If two setoids are in bijective correspondence, then there is an
75
-- inverse between them.
78
∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
79
Bijection From To → Inverse From To
80
fromBijection b = record
82
; from = Bijection.from b
84
{ left-inverse-of = Bijection.left-inverse-of b
85
; right-inverse-of = Bijection.right-inverse-of b
89
------------------------------------------------------------------------
92
map : ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂}
94
{From′ : Setoid f₁′ f₂′} {To′ : Setoid t₁′ t₂′} →
95
(t : (From ⟶ To) → (From′ ⟶ To′)) →
96
(f : (To ⟶ From) → (To′ ⟶ From′)) →
97
(∀ {to from} → from InverseOf to → f from InverseOf t to) →
98
Inverse From To → Inverse From′ To′
99
map t f pres eq = record
102
; inverse-of = pres inverse-of
103
} where open Inverse eq
105
zip : ∀ {f₁₁ f₂₁ t₁₁ t₂₁}
106
{From₁ : Setoid f₁₁ f₂₁} {To₁ : Setoid t₁₁ t₂₁}
108
{From₂ : Setoid f₁₂ f₂₂} {To₂ : Setoid t₁₂ t₂₂}
109
{f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
110
(t : (From₁ ⟶ To₁) → (From₂ ⟶ To₂) → (From ⟶ To)) →
111
(f : (To₁ ⟶ From₁) → (To₂ ⟶ From₂) → (To ⟶ From)) →
112
(∀ {to₁ from₁ to₂ from₂} →
113
from₁ InverseOf to₁ → from₂ InverseOf to₂ →
114
f from₁ from₂ InverseOf t to₁ to₂) →
115
Inverse From₁ To₁ → Inverse From₂ To₂ → Inverse From To
116
zip t f pres eq₁ eq₂ = record
117
{ to = t (to eq₁) (to eq₂)
118
; from = f (from eq₁) (from eq₂)
119
; inverse-of = pres (inverse-of eq₁) (inverse-of eq₂)
122
------------------------------------------------------------------------
123
-- Inverse is an equivalence relation
125
-- Identity and composition (reflexivity and transitivity).
127
id : ∀ {s₁ s₂} → Reflexive (Inverse {s₁} {s₂})
131
; inverse-of = record
132
{ left-inverse-of = LeftInverse.left-inverse-of id′
133
; right-inverse-of = LeftInverse.left-inverse-of id′
135
} where id′ = Left.id {S = S}
139
_∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂} →
140
TransFlip (Inverse {f₁} {f₂} {m₁} {m₂})
141
(Inverse {m₁} {m₂} {t₁} {t₂})
142
(Inverse {f₁} {f₂} {t₁} {t₂})
145
; from = from g ⟪∘⟫ from f
146
; inverse-of = record
147
{ left-inverse-of = LeftInverse.left-inverse-of (Left._∘_ (left-inverse f) (left-inverse g))
148
; right-inverse-of = LeftInverse.left-inverse-of (Left._∘_ (right-inverse g) (right-inverse f))
157
sym : ∀ {f₁ f₂ t₁ t₂} →
158
Sym (Inverse {f₁} {f₂} {t₁} {t₂}) (Inverse {t₁} {t₂} {f₁} {f₂})
162
; inverse-of = record
163
{ left-inverse-of = right-inverse-of
164
; right-inverse-of = left-inverse-of
166
} where open Inverse inv
168
-- For fixed universe levels we can construct a setoid.
170
setoid : (s₁ s₂ : Level) → Setoid (suc (s₁ ⊔ s₂)) (s₁ ⊔ s₂)
171
setoid s₁ s₂ = record
172
{ Carrier = Setoid s₁ s₂
175
record {refl = id; sym = Dummy.sym; trans = flip _∘_}
178
------------------------------------------------------------------------
179
-- A generalisation which includes both _⇔_ and _⇿_
181
-- There are two kinds of "isomorphisms": equivalences and inverses.
183
data Kind : Set where
184
equivalent inverse : Kind
186
Isomorphism : Kind → ∀ {ℓ₁ ℓ₂} → Set ℓ₁ → Set ℓ₂ → Set _
187
Isomorphism inverse A B = Inverse (P.setoid A) (P.setoid B)
188
Isomorphism equivalent A B = Equivalent (P.setoid A) (P.setoid B)
190
-- Inverses are stronger, equivalences weaker.
192
⇿⇒ : ∀ {k x y} {X : Set x} {Y : Set y} →
193
Isomorphism inverse X Y → Isomorphism k X Y
194
⇿⇒ {inverse} = Fun.id
195
⇿⇒ {equivalent} = Inverse.equivalent
197
⇒⇔ : ∀ {k x y} {X : Set x} {Y : Set y} →
198
Isomorphism k X Y → Isomorphism equivalent X Y
199
⇒⇔ {inverse} = Inverse.equivalent
200
⇒⇔ {equivalent} = Fun.id
202
-- Equational reasoning for isomorphisms.
204
module EquationalReasoning where
208
refl : ∀ {k ℓ} → Reflexive (Isomorphism k {ℓ})
210
refl {equivalent} = Eq.id
212
trans : ∀ {k ℓ₁ ℓ₂ ℓ₃} →
213
Trans (Isomorphism k {ℓ₁} {ℓ₂})
214
(Isomorphism k {ℓ₂} {ℓ₃})
215
(Isomorphism k {ℓ₁} {ℓ₃})
216
trans {inverse} = flip _∘_
217
trans {equivalent} = flip Eq._∘_
220
Sym (Isomorphism k {ℓ₁} {ℓ₂})
221
(Isomorphism k {ℓ₂} {ℓ₁})
222
sym {inverse} = Dummy.sym
223
sym {equivalent} = Eq.sym
226
infixr 2 _≈⟨_⟩_ _⇿⟨_⟩_
228
_≈⟨_⟩_ : ∀ {k x y z} (X : Set x) {Y : Set y} {Z : Set z} →
229
Isomorphism k X Y → Isomorphism k Y Z → Isomorphism k X Z
230
_ ≈⟨ X≈Y ⟩ Y≈Z = trans X≈Y Y≈Z
232
_⇿⟨_⟩_ : ∀ {k x y z} (X : Set x) {Y : Set y} {Z : Set z} →
233
X ⇿ Y → Isomorphism k Y Z → Isomorphism k X Z
234
X ⇿⟨ X⇿Y ⟩ Y⇔Z = X ≈⟨ ⇿⇒ X⇿Y ⟩ Y⇔Z
236
_∎ : ∀ {k x} (X : Set x) → Isomorphism k X X
239
-- For fixed universe levels we can construct a setoid.
241
Isomorphism-setoid : Kind → (ℓ : Level) → Setoid _ _
242
Isomorphism-setoid k ℓ = record
244
; _≈_ = Isomorphism k
246
record {refl = _ ∎; sym = sym; trans = _≈⟨_⟩_ _}
247
} where open EquationalReasoning
249
-- Every unary relation induces an equivalence relation. (No claim is
250
-- made that this relation is unique.)
252
InducedEquivalence₁ : Kind → ∀ {a s} {A : Set a}
253
(S : A → Set s) → Setoid _ _
254
InducedEquivalence₁ k S = record
255
{ _≈_ = λ x y → Isomorphism k (S x) (S y)
256
; isEquivalence = record {refl = refl; sym = sym; trans = trans}
257
} where open Setoid (Isomorphism-setoid _ _)
259
-- Every binary relation induces an equivalence relation. (No claim is
260
-- made that this relation is unique.)
262
InducedEquivalence₂ : Kind → ∀ {a b s} {A : Set a} {B : Set b}
263
(_S_ : A → B → Set s) → Setoid _ _
264
InducedEquivalence₂ k _S_ = record
265
{ _≈_ = λ x y → ∀ {z} → Isomorphism k (z S x) (z S y)
266
; isEquivalence = record
268
; sym = λ i≈j → sym i≈j
269
; trans = λ i≈j j≈k → trans i≈j j≈k
271
} where open Setoid (Isomorphism-setoid _ _)
added
removed
src/Function/Inverse.agda
