1
------------------------------------------------------------------------
2
-- Various basic type isomorphisms
3
------------------------------------------------------------------------
5
{-# OPTIONS --universe-polymorphism #-}
7
module Function.Inverse.TypeIsomorphisms where
10
import Algebra.FunctionProperties as FP
11
open import Data.Empty
12
open import Data.Product as Prod hiding (swap)
13
open import Data.Sum as Sum
17
open import Function.Equality using (_⟨$⟩_)
18
open import Function.Equivalence
19
using (_⇔_; equivalent; module Equivalent)
20
open import Function.Inverse as Inv
21
using (Kind; Isomorphism; _⇿_; module Inverse)
22
open import Relation.Binary
23
open import Relation.Binary.Product.Pointwise
24
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)
25
open import Relation.Binary.Sum
26
open import Relation.Nullary
28
------------------------------------------------------------------------
29
-- ⊥, ⊤, _×_ and _⊎_ form a commutative semiring
31
×-CommutativeMonoid : Kind → (ℓ : Level) → CommutativeMonoid _ _
32
×-CommutativeMonoid k ℓ = record
37
; isCommutativeMonoid = record
38
{ isSemigroup = record
39
{ isEquivalence = Setoid.isEquivalence $
40
Inv.Isomorphism-setoid k ℓ
41
; assoc = λ A B C → Inv.⇿⇒ $ assoc A B C
44
; identityˡ = λ A → Inv.⇿⇒ $ left-identity A
45
; comm = λ A B → Inv.⇿⇒ $ comm A B
51
×-cong : ∀ k {A B C D : Set ℓ} →
52
Isomorphism k A B → Isomorphism k C D →
53
Isomorphism k (A × C) (B × D)
54
×-cong Inv.equivalent = _×-⇔_
55
×-cong Inv.inverse = _×-⇿_
57
left-identity : LeftIdentity (Lift {ℓ = ℓ} ⊤) _×_
58
left-identity _ = record
59
{ to = P.→-to-⟶ $ proj₂ {a = ℓ} {b = ℓ}
60
; from = P.→-to-⟶ {b₁ = ℓ} λ y → _ , y
62
{ left-inverse-of = λ _ → P.refl
63
; right-inverse-of = λ _ → P.refl
67
assoc : Associative _×_
69
{ to = P.→-to-⟶ {a = ℓ} {b₁ = ℓ} λ t → (proj₁ (proj₁ t) , (proj₂ (proj₁ t) , proj₂ t))
70
; from = P.→-to-⟶ {a = ℓ} {b₁ = ℓ} λ t → ((proj₁ t , proj₁ (proj₂ t)) , proj₂ (proj₂ t))
72
{ left-inverse-of = λ _ → P.refl
73
; right-inverse-of = λ _ → P.refl
77
comm : Commutative _×_
79
{ to = P.→-to-⟶ $ Prod.swap {a = ℓ} {b = ℓ}
80
; from = P.→-to-⟶ $ Prod.swap {a = ℓ} {b = ℓ}
82
{ left-inverse-of = λ _ → P.refl
83
; right-inverse-of = λ _ → P.refl
87
⊎-CommutativeMonoid : Kind → (ℓ : Level) → CommutativeMonoid _ _
88
⊎-CommutativeMonoid k ℓ = record
93
; isCommutativeMonoid = record
94
{ isSemigroup = record
95
{ isEquivalence = Setoid.isEquivalence $
96
Inv.Isomorphism-setoid k ℓ
97
; assoc = λ A B C → Inv.⇿⇒ $ assoc A B C
100
; identityˡ = λ A → Inv.⇿⇒ $ left-identity A
101
; comm = λ A B → Inv.⇿⇒ $ comm A B
107
⊎-cong : ∀ k {A B C D : Set ℓ} →
108
Isomorphism k A B → Isomorphism k C D →
109
Isomorphism k (A ⊎ C) (B ⊎ D)
110
⊎-cong Inv.equivalent = _⊎-⇔_
111
⊎-cong Inv.inverse = _⊎-⇿_
113
left-identity : LeftIdentity (Lift ⊥) (_⊎_ {a = ℓ} {b = ℓ})
114
left-identity A = record
116
; from = P.→-to-⟶ from
117
; inverse-of = record
118
{ right-inverse-of = λ _ → P.refl
120
[ ⊥-elim {Whatever = _ ≡ _} ∘ lower , (λ _ → P.refl) ]
124
to : Lift {ℓ = ℓ} ⊥ ⊎ A → A
125
to = [ (λ ()) ∘′ lower , id ]
127
from : A → Lift {ℓ = ℓ} ⊥ ⊎ A
130
assoc : Associative _⊎_
133
; from = P.→-to-⟶ from
134
; inverse-of = record
135
{ left-inverse-of = [ [ (λ _ → P.refl) , (λ _ → P.refl) ] , (λ _ → P.refl) ]
136
; right-inverse-of = [ (λ _ → P.refl) , [ (λ _ → P.refl) , (λ _ → P.refl) ] ]
140
to : (A ⊎ B) ⊎ C → A ⊎ (B ⊎ C)
141
to = [ [ inj₁ , inj₂ ∘ inj₁ ] , inj₂ ∘ inj₂ ]
143
from : A ⊎ (B ⊎ C) → (A ⊎ B) ⊎ C
144
from = [ inj₁ ∘ inj₁ , [ inj₁ ∘ inj₂ , inj₂ ] ]
146
comm : Commutative _⊎_
149
; from = P.→-to-⟶ swap
150
; inverse-of = record
151
{ left-inverse-of = inv
152
; right-inverse-of = inv
156
swap : {A B : Set ℓ} → A ⊎ B → B ⊎ A
157
swap = [ inj₂ , inj₁ ]
159
inv : ∀ {A B} → swap ∘ swap {A} {B} ≗ id
160
inv = [ (λ _ → P.refl) , (λ _ → P.refl) ]
162
×⊎-CommutativeSemiring : Kind → (ℓ : Level) → CommutativeSemiring _ _
163
×⊎-CommutativeSemiring k ℓ = record
165
; _≈_ = Isomorphism k
170
; isCommutativeSemiring = record
171
{ +-isCommutativeMonoid = isCommutativeMonoid $
172
⊎-CommutativeMonoid k ℓ
173
; *-isCommutativeMonoid = isCommutativeMonoid $
174
×-CommutativeMonoid k ℓ
175
; distribʳ = λ A B C → Inv.⇿⇒ $ right-distrib A B C
176
; zeroˡ = λ A → Inv.⇿⇒ $ left-zero A
180
open CommutativeMonoid
183
left-zero : LeftZero (Lift ⊥) (_×_ {a = ℓ} {b = ℓ})
185
{ to = P.→-to-⟶ $ proj₁ {a = ℓ} {b = ℓ}
186
; from = P.→-to-⟶ (⊥-elim ∘′ lower)
187
; inverse-of = record
188
{ left-inverse-of = λ p → ⊥-elim (lower $ proj₁ p)
189
; right-inverse-of = λ x → ⊥-elim (lower x)
193
right-distrib : _×_ DistributesOverʳ _⊎_
194
right-distrib A B C = record
196
; from = P.→-to-⟶ from
197
; inverse-of = record
198
{ right-inverse-of = [ (λ _ → P.refl) , (λ _ → P.refl) ]
200
uncurry [ (λ _ _ → P.refl) , (λ _ _ → P.refl) ]
204
to : (B ⊎ C) × A → B × A ⊎ C × A
205
to = uncurry [ curry inj₁ , curry inj₂ ]
207
from : B × A ⊎ C × A → (B ⊎ C) × A
208
from = [ Prod.map inj₁ id , Prod.map inj₂ id ]
210
------------------------------------------------------------------------
211
-- Some reordering lemmas
213
ΠΠ⇿ΠΠ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p) →
214
((x : A) (y : B) → P x y) ⇿ ((y : B) (x : A) → P x y)
216
{ to = P.→-to-⟶ λ f x y → f y x
217
; from = P.→-to-⟶ λ f y x → f x y
218
; inverse-of = record
219
{ left-inverse-of = λ _ → P.refl
220
; right-inverse-of = λ _ → P.refl
224
∃∃⇿∃∃ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p) →
225
(∃₂ λ x y → P x y) ⇿ (∃₂ λ y x → P x y)
226
∃∃⇿∃∃ {a} {b} {p} _ = record
227
{ to = P.→-to-⟶ {a = ℓ} λ p → (proj₁ (proj₂ p) , proj₁ p , proj₂ (proj₂ p))
228
; from = P.→-to-⟶ {a = ℓ} λ p → (proj₁ (proj₂ p) , proj₁ p , proj₂ (proj₂ p))
229
; inverse-of = record
230
{ left-inverse-of = λ _ → P.refl
231
; right-inverse-of = λ _ → P.refl
233
} where ℓ = p ⊔ (b ⊔ a)
235
------------------------------------------------------------------------
236
-- Implicit and explicit function spaces are isomorphic
238
Π⇿Π : ∀ {a b} {A : Set a} {B : A → Set b} →
239
((x : A) → B x) ⇿ ({x : A} → B x)
241
{ to = P.→-to-⟶ λ f {x} → f x
242
; from = P.→-to-⟶ λ f x → f {x}
243
; inverse-of = record
244
{ left-inverse-of = λ _ → P.refl
245
; right-inverse-of = λ _ → P.refl
249
------------------------------------------------------------------------
250
-- _→_ preserves isomorphisms
253
∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
254
A ⇔ B → C ⇔ D → (A → C) ⇔ (B → D)
255
A⇔B →-cong-⇔ C⇔D = record
256
{ to = P.→-to-⟶ λ f x →
257
Equivalent.to C⇔D ⟨$⟩ f (Equivalent.from A⇔B ⟨$⟩ x)
258
; from = P.→-to-⟶ λ f x →
259
Equivalent.from C⇔D ⟨$⟩ f (Equivalent.to A⇔B ⟨$⟩ x)
264
P.Extensionality a c → P.Extensionality b d →
265
∀ {k} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
266
Isomorphism k A B → Isomorphism k C D → Isomorphism k (A → C) (B → D)
267
→-cong extAC extBD {Inv.equivalent} A⇔B C⇔D = A⇔B →-cong-⇔ C⇔D
268
→-cong extAC extBD {Inv.inverse} A⇿B C⇿D = record
269
{ to = Equivalent.to A→C⇔B→D
270
; from = Equivalent.from A→C⇔B→D
271
; inverse-of = record
272
{ left-inverse-of = λ f → extAC λ x → begin
273
Inverse.from C⇿D ⟨$⟩ (Inverse.to C⇿D ⟨$⟩
274
f (Inverse.from A⇿B ⟨$⟩ (Inverse.to A⇿B ⟨$⟩ x))) ≡⟨ Inverse.left-inverse-of C⇿D _ ⟩
275
f (Inverse.from A⇿B ⟨$⟩ (Inverse.to A⇿B ⟨$⟩ x)) ≡⟨ P.cong f $ Inverse.left-inverse-of A⇿B x ⟩
277
; right-inverse-of = λ f → extBD λ x → begin
278
Inverse.to C⇿D ⟨$⟩ (Inverse.from C⇿D ⟨$⟩
279
f (Inverse.to A⇿B ⟨$⟩ (Inverse.from A⇿B ⟨$⟩ x))) ≡⟨ Inverse.right-inverse-of C⇿D _ ⟩
280
f (Inverse.to A⇿B ⟨$⟩ (Inverse.from A⇿B ⟨$⟩ x)) ≡⟨ P.cong f $ Inverse.right-inverse-of A⇿B x ⟩
286
A→C⇔B→D = Inv.⇿⇒ A⇿B →-cong-⇔ Inv.⇿⇒ C⇿D
288
------------------------------------------------------------------------
289
-- ¬_ preserves isomorphisms
291
¬-cong-⇔ : ∀ {a b} {A : Set a} {B : Set b} →
292
A ⇔ B → (¬ A) ⇔ (¬ B)
293
¬-cong-⇔ A⇔B = A⇔B →-cong-⇔ (⊥ ∎)
294
where open Inv.EquationalReasoning
297
P.Extensionality a zero → P.Extensionality b zero →
298
∀ {k} {A : Set a} {B : Set b} →
299
Isomorphism k A B → Isomorphism k (¬ A) (¬ B)
300
¬-cong extA extB A≈B = →-cong extA extB A≈B (⊥ ∎)
301
where open Inv.EquationalReasoning
303
------------------------------------------------------------------------
306
-- The type of the following proof is a bit more general.
309
∀ {k a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
310
Isomorphism k A B → Isomorphism k C D →
311
Isomorphism k A C ⇔ Isomorphism k B D
312
Isomorphism-cong {A = A} {B} {C} {D} A≈B C≈D =
313
equivalent (λ A≈C → B ≈⟨ sym A≈B ⟩
321
where open Inv.EquationalReasoning
added
removed
src/Function/Inverse/TypeIsomorphisms.agda
