-
Notifications
You must be signed in to change notification settings - Fork 1
/
Monoidal.agda
128 lines (114 loc) · 4.78 KB
/
Monoidal.agda
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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
{-# OPTIONS --without-K --exact-split --rewriting #-}
module Pi.UFin.Monoidal where
open import HoTT
open import homotopy.FinSet public
open import Pi.UFin.Base
open import Pi.Common.Misc as N
open import Pi.Common.Extra
⊔-comm : (A B : Type₀) -> (A ⊔ B) ≃ (B ⊔ A)
⊔-comm A B = equiv f g f-g g-f
where f : (A ⊔ B) -> (B ⊔ A)
f (inl x) = inr x
f (inr x) = inl x
g : (B ⊔ A) -> (A ⊔ B)
g (inl x) = inr x
g (inr x) = inl x
f-g : ∀ x -> f (g x) == x
f-g (inl x) = idp
f-g (inr x) = idp
g-f : ∀ x -> g (f x) == x
g-f (inl x) = idp
g-f (inr x) = idp
⊔-assoc : (A B C : Type₀) -> (A ⊔ B) ⊔ C ≃ A ⊔ (B ⊔ C)
⊔-assoc A B C = equiv f g f-g g-f
where f : (A ⊔ B) ⊔ C -> A ⊔ (B ⊔ C)
f (inl (inl x)) = inl x
f (inl (inr x)) = inr (inl x)
f (inr x) = inr (inr x)
g : A ⊔ (B ⊔ C) -> (A ⊔ B) ⊔ C
g (inl x) = inl (inl x)
g (inr (inl x)) = inl (inr x)
g (inr (inr x)) = inr x
f-g : ∀ x -> f (g x) == x
f-g (inl x) = idp
f-g (inr (inl x)) = idp
f-g (inr (inr x)) = idp
g-f : ∀ x -> g (f x) == x
g-f (inl (inl x)) = idp
g-f (inl (inr x)) = idp
g-f (inr x) = idp
⊔-≃ : {A B C D : Type₀} → (A ≃ B) → (C ≃ D) → (A ⊔ C) ≃ (B ⊔ D)
⊔-≃ {A} {B} {C} {D} e₁ e₂ = equiv f g f-g g-f
where f : A ⊔ C → B ⊔ D
f (inl a) = inl (–> e₁ a)
f (inr c) = inr (–> e₂ c)
g : B ⊔ D → A ⊔ C
g (inl b) = inl (<– e₁ b)
g (inr d) = inr (<– e₂ d)
f-g : (x : B ⊔ D) → f (g x) == x
f-g (inl b) = ap inl (<–-inv-r e₁ b)
f-g (inr d) = ap inr (<–-inv-r e₂ d)
g-f : (x : A ⊔ C) → g (f x) == x
g-f (inl a) = ap inl (<–-inv-l e₁ a)
g-f (inr c) = ap inr (<–-inv-l e₂ c)
Fin-⊔ : {n m : ℕ} → (Fin n ⊔ Fin m) ≃ Fin (n + m)
Fin-⊔ {O} {m} =
⊔₁-Empty (Fin m) ∘e
⊔-≃ Fin-equiv-Empty (ide (Fin m))
Fin-⊔ {S n} {m} =
Fin-equiv-Coprod {n + m} ⁻¹ ∘e
⊔-≃ (Fin-⊔ {n} {m}) (ide ⊤) ∘e
⊔-assoc (Fin n) (Fin m) ⊤ ⁻¹ ∘e
⊔-≃ (ide (Fin n)) (⊔-comm ⊤ (Fin m)) ∘e
⊔-assoc (Fin n) ⊤ (Fin m) ∘e
⊔-≃ (Fin-equiv-Coprod {n}) (ide (Fin m))
_∪_ : FinSet -> FinSet → FinSet
(X , ϕ) ∪ (Y , ψ) = X ⊔ Y , Trunc-fmap2 tx ϕ ψ
where
tx : Σ ℕ (λ n → Fin n == X) → Σ ℕ (λ n → Fin n == Y) → Σ ℕ (λ n → Fin n == X ⊔ Y)
tx (n , α) (m , β)= (n + m) , ua ((Fin-⊔ ∘e transport2-equiv (λ x y -> x ⊔ y) (! α) (! β)) ⁻¹)
×₁-Empty : ∀ {i} (A : Type i) → Empty × A ≃ Empty
×₁-Empty A = equiv (λ { ((), a) }) (λ ()) (λ ()) (λ { ((), a) })
×₁-Unit : ∀ {i} (A : Type i) → Unit × A ≃ A
×₁-Unit A = equiv snd (λ a → tt , a) (λ a → idp) (λ { (tt , a) → idp })
×-≃ : {A B C D : Type₀} → (A ≃ B) → (C ≃ D) → (A × C) ≃ (B × D)
×-≃ {A} {B} {C} {D} e₁ e₂ = equiv f g f-g g-f
where f : (A × C) → (B × D)
f (a , c) = –> e₁ a , –> e₂ c
g : (B × D) → (A × C)
g (b , d) = <– e₁ b , <– e₂ d
f-g : (x : B × D) → f (g x) == x
f-g (b , d) = pair= (<–-inv-r e₁ b) (↓-cst-in (<–-inv-r e₂ d))
g-f : (x : A × C) → g (f x) == x
g-f (a , c) = pair= (<–-inv-l e₁ a) (↓-cst-in (<–-inv-l e₂ c))
×-⊔-distrib : (A B C : Type₀) → (A ⊔ B) × C ≃ (A × C) ⊔ (B × C)
×-⊔-distrib A B C = equiv f g f-g g-f
where f : (A ⊔ B) × C → (A × C) ⊔ (B × C)
f (inl a , c) = inl (a , c)
f (inr b , c) = inr (b , c)
g : (A × C) ⊔ (B × C) → (A ⊔ B) × C
g (inl (a , c)) = inl a , c
g (inr (b , c)) = inr b , c
f-g : (x : (A × C) ⊔ B × C) → f (g x) == x
f-g (inl (a , c)) = idp
f-g (inr (b , c)) = idp
g-f : (x : (A ⊔ B) × C) → g (f x) == x
g-f (inl a , c) = idp
g-f (inr b , c) = idp
Fin-× : {n m : ℕ} → (Fin n × Fin m) ≃ Fin (n N.* m)
Fin-× {O} {m} =
Fin-equiv-Empty ⁻¹ ∘e
×₁-Empty (Fin m) ∘e
×-≃ Fin-equiv-Empty (ide (Fin m))
Fin-× {S n} {m} =
Fin-⊔ {m} {n N.* m} ∘e
⊔-≃ (ide (Fin m)) (Fin-× {n} {m}) ∘e
⊔-comm (Fin n × Fin m) (Fin m) ∘e
⊔-≃ (ide _) (×₁-Unit (Fin m)) ∘e
×-⊔-distrib (Fin n) ⊤ (Fin m) ∘e
×-≃ Fin-equiv-Coprod (ide (Fin m))
_⊓_ : FinSet -> FinSet → FinSet
(X , ϕ) ⊓ (Y , ψ) = X × Y , Trunc-fmap2 tx ϕ ψ
where
tx : Σ ℕ (λ n → Fin n == X) → Σ ℕ (λ n → Fin n == Y) → Σ ℕ (λ n → Fin n == X × Y)
tx (n , α) (m , β)= (n N.* m) , ua ((Fin-× ∘e transport2-equiv (λ x y -> x × y) (! α) (! β)) ⁻¹)