-
Notifications
You must be signed in to change notification settings - Fork 3
/
Coerce.agda
226 lines (206 loc) · 11.2 KB
/
Coerce.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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
{-# OPTIONS --no-termination-check #-}
module OTT.Coerce where
open import OTT.Core
coerceFamℕ : ∀ {n m} -> (A : ℕ -> Set) -> ⟦ n ≟ⁿ m ⟧ -> A n -> A m
coerceFamℕ {0} {0} A q x = x
coerceFamℕ {suc _} {suc _} A q x = coerceFamℕ (A ∘ suc) q x
coerceFamℕ {0} {suc _} A () x
coerceFamℕ {suc _} {0} A () x
coerceFamLevel : ∀ {a b} {α : Level a} {β : Level b}
-> (A : ∀ {a} -> Level a -> Set) -> ⟦ α ≟ˡ β ⟧ -> A α -> A β
coerceFamLevel {α = lzero } {lzero } A q x = x
coerceFamLevel {α = lsuc _} {lsuc _} A q x = coerceFamLevel (A ∘ lsuc) q x
coerceFamLevel {α = lzero } {lsuc _} A () x
coerceFamLevel {α = lsuc _} {lzero } A () x
meta-eq : ∀ {a b} {β : Level b} -> (α : Level a) -> ⟦ α ≟ˡ β ⟧ -> a ≡ b
meta-eq α q = coerceFamLevel {α = α} (λ {b} _ -> _ ≡ b) q prefl
Coerce : ∀ {a b} {α : Level a} {β : Level b} -> ⟦ α ≟ˡ β ⟧ -> Univ α -> Univ β
Coerce = coerceFamLevel Univ
mutual
coerce : ∀ {a b} {α : Level a} {β : Level b} {A : Univ α} {B : Univ β} -> ⟦ A ≈ B ⇒ A ⇒ B ⟧
coerce {α = lzero } {lzero } (f , _) = f
coerce {α = lsuc _} {lsuc _} q = coerce′ q
coerce {α = lzero } {lsuc _} ()
coerce {α = lsuc _} {lzero } ()
coerce′ : ∀ {a b} {α : Level a} {β : Level b} {A : Univ α} {B : Univ β} -> ⟦ A ≃ B ⇒ A ⇒ B ⟧
coerce′ {A = bot } {bot } q ()
coerce′ {A = top } {top } q tt = tt
coerce′ {A = nat } {nat } q n = n
coerce′ {A = enum n₁ } {enum n₂ } q e = coerceFamℕ (Apply Enum) q e
coerce′ {A = univ α₁ } {univ α₂ } q A = Coerce q A
coerce′ {A = σ A₁ B₁ } {σ A₂ B₂ } q p = let q₁ , q₂ = q ; x , y = p in
coerce q₁ x , coerce (q₂ x (coerce q₁ x) (coherence q₁ x)) y
coerce′ {A = π A₁ B₁ } {π A₂ B₂ } q f = let q₁ , q₂ = q in
λ x -> coerce (q₂ (coerce q₁ x) x (coherence q₁ x)) (f (coerce q₁ x))
coerce′ {A = desc _ α} {desc _ _} q D = let qI , qα = q in coerceDesc qI (meta-eq α qα) D
coerce′ {A = imu _ _ } {imu _ _ } q d = let qD , qi = q in coerceMu qD qi d
coerce′ {A = bot } {top } ()
coerce′ {A = bot } {nat } ()
coerce′ {A = bot } {enum _ } ()
coerce′ {A = bot } {univ _ } ()
coerce′ {A = bot } {σ _ _ } ()
coerce′ {A = bot } {π _ _ } ()
coerce′ {A = bot } {desc _ _} ()
coerce′ {A = bot } {imu _ _ } ()
coerce′ {A = top } {bot } ()
coerce′ {A = top } {nat } ()
coerce′ {A = top } {enum _ } ()
coerce′ {A = top } {univ _ } ()
coerce′ {A = top } {σ _ _ } ()
coerce′ {A = top } {π _ _ } ()
coerce′ {A = top } {desc _ _} ()
coerce′ {A = top } {imu _ _ } ()
coerce′ {A = nat } {bot } ()
coerce′ {A = nat } {top } ()
coerce′ {A = nat } {enum _ } ()
coerce′ {A = nat } {univ _ } ()
coerce′ {A = nat } {σ _ _ } ()
coerce′ {A = nat } {π _ _ } ()
coerce′ {A = nat } {desc _ _} ()
coerce′ {A = nat } {imu _ _ } ()
coerce′ {A = enum _ } {bot } ()
coerce′ {A = enum _ } {top } ()
coerce′ {A = enum _ } {nat } ()
coerce′ {A = enum _ } {univ _ } ()
coerce′ {A = enum _ } {σ _ _ } ()
coerce′ {A = enum _ } {π _ _ } ()
coerce′ {A = enum _ } {desc _ _} ()
coerce′ {A = enum _ } {imu _ _ } ()
coerce′ {A = univ _ } {bot } ()
coerce′ {A = univ _ } {top } ()
coerce′ {A = univ _ } {nat } ()
coerce′ {A = univ _ } {enum _ } ()
coerce′ {A = univ _ } {σ _ _ } ()
coerce′ {A = univ _ } {π _ _ } ()
coerce′ {A = univ _ } {desc _ _} ()
coerce′ {A = univ _ } {imu _ _ } ()
coerce′ {A = σ _ _ } {bot } ()
coerce′ {A = σ _ _ } {top } ()
coerce′ {A = σ _ _ } {nat } ()
coerce′ {A = σ _ _ } {enum _ } ()
coerce′ {A = σ _ _ } {univ _ } ()
coerce′ {A = σ _ _ } {π _ _ } ()
coerce′ {A = σ _ _ } {desc _ _} ()
coerce′ {A = σ _ _ } {imu _ _ } ()
coerce′ {A = π _ _ } {bot } ()
coerce′ {A = π _ _ } {top } ()
coerce′ {A = π _ _ } {nat } ()
coerce′ {A = π _ _ } {enum _ } ()
coerce′ {A = π _ _ } {univ _ } ()
coerce′ {A = π _ _ } {σ _ _ } ()
coerce′ {A = π _ _ } {desc _ _} ()
coerce′ {A = π _ _ } {imu _ _ } ()
coerce′ {A = desc _ _} {bot } ()
coerce′ {A = desc _ _} {top } ()
coerce′ {A = desc _ _} {nat } ()
coerce′ {A = desc _ _} {enum _ } ()
coerce′ {A = desc _ _} {univ _ } ()
coerce′ {A = desc _ _} {σ _ _ } ()
coerce′ {A = desc _ _} {π _ _ } ()
coerce′ {A = desc _ _} {imu _ _ } ()
coerce′ {A = imu _ _ } {bot } ()
coerce′ {A = imu _ _ } {top } ()
coerce′ {A = imu _ _ } {nat } ()
coerce′ {A = imu _ _ } {enum _ } ()
coerce′ {A = imu _ _ } {univ _ } ()
coerce′ {A = imu _ _ } {σ _ _ } ()
coerce′ {A = imu _ _ } {π _ _ } ()
coerce′ {A = imu _ _ } {desc _ _} ()
-- (almost) generated by http://ideone.com/ltrf04
coerceDesc : ∀ {i₁ i₂ a₁ a₂} {ι₁ : Level i₁} {ι₂ : Level i₂}
{α₁ : Level a₁} {α₂ : Level a₂} {I₁ : Type ι₁} {I₂ : Type ι₂}
-> ⟦ I₁ ≃ I₂ ⟧ -> a₁ ≡ a₂ -> Desc I₁ α₁ -> Desc I₂ α₂
coerceDesc qI qa (var i) = var (coerce qI i)
coerceDesc qI qa (π {a} {{q}} A D) =
π {{ptrans (pright (pcong (a ⊔ₘ_) qa) q) qa}} A (coerceDesc qI qa ∘ D)
coerceDesc qI qa (D ⊛ E) = coerceDesc qI qa D ⊛ coerceDesc qI qa E
coerceSem : ∀ {i₁ i₂ a₁ a₂ b₁ b₂}
{ι₁ : Level i₁} {ι₂ : Level i₂} {α₁ : Level a₁} {α₂ : Level a₂}
{β₁ : Level b₁} {β₂ : Level b₂} {I₁ : Type ι₁} {I₂ : Type ι₂}
{B₁ : ⟦ I₁ ⟧ -> Univ β₁} {B₂ : ⟦ I₂ ⟧ -> Univ β₂}
-> (D₁ : Desc I₁ α₁)
-> (D₂ : Desc I₂ α₂)
-> ⟦ D₁ ≅ᵈ D₂ ⟧
-> ⟦ B₁ ≅ B₂ ⟧
-> (⟦ D₁ ⟧ᵈ ⟦ B₁ ⟧ⁱ)
-> (⟦ D₂ ⟧ᵈ ⟦ B₂ ⟧ⁱ)
coerceSem (var i₁) (var i₂) qi qB x = coerce (qB i₁ i₂ qi) x
coerceSem (π A₁ D₁) (π A₂ D₂) (qA , qD) qB f = λ x ->
let qA′ = sym A₁ {A₂} qA
x′ = coerce qA′ x
in coerceSem (D₁ x′) (D₂ x) (qD x′ x (sym x (coherence qA′ x))) qB (f x′)
coerceSem (D₁ ⊛ E₁) (D₂ ⊛ E₂) (qD , qE) qB (s , t) =
coerceSem D₁ D₂ qD qB s , coerceSem E₁ E₂ qE qB t
coerceSem (var _) (π _ _) ()
coerceSem (var _) (_ ⊛ _) ()
coerceSem (π _ _) (var _) ()
coerceSem (π _ _) (_ ⊛ _) ()
coerceSem (_ ⊛ _) (var _) ()
coerceSem (_ ⊛ _) (π _ _) ()
coerceExtend : ∀ {i₁ i₂ a₁ a₂ b₁ b₂}
{ι₁ : Level i₁} {ι₂ : Level i₂} {α₁ : Level a₁} {α₂ : Level a₂}
{β₁ : Level b₁} {β₂ : Level b₂} {I₁ : Type ι₁} {I₂ : Type ι₂}
{B₁ : ⟦ I₁ ⟧ -> Univ β₁} {B₂ : ⟦ I₂ ⟧ -> Univ β₂} {j₁ j₂}
-> (D₁ : Desc I₁ α₁)
-> (D₂ : Desc I₂ α₂)
-> ⟦ D₁ ≅ᵈ D₂ ⟧
-> ⟦ B₁ ≅ B₂ ⟧
-> ⟦ j₁ ≅ j₂ ⟧
-> Extend D₁ ⟦ B₁ ⟧ⁱ j₁
-> Extend D₂ ⟦ B₂ ⟧ⁱ j₂
coerceExtend (var i₁) (var i₂) qi qB qj qij = trans i₂ (right i₁ qi qij) qj
coerceExtend (π A₁ D₁) (π A₂ D₂) (qA , qD) qB qi (x , e) = let x′ = coerce qA x in
x′ , coerceExtend (D₁ x) (D₂ x′) (qD x x′ (coherence qA x)) qB qi e
coerceExtend (D₁ ⊛ E₁) (D₂ ⊛ E₂) (qD , qE) qB qi (s , e) =
coerceSem D₁ D₂ qD qB s , coerceExtend E₁ E₂ qE qB qi e
coerceExtend (var _) (π _ _) ()
coerceExtend (var _) (_ ⊛ _) ()
coerceExtend (π _ _) (var _) ()
coerceExtend (π _ _) (_ ⊛ _) ()
coerceExtend (_ ⊛ _) (var _) ()
coerceExtend (_ ⊛ _) (π _ _) ()
coerceMu : ∀ {i₁ i₂ a₁ a₂} {ι₁ : Level i₁} {ι₂ : Level i₂} {α₁ : Level a₁} {α₂ : Level a₂}
{I₁ : Type ι₁} {I₂ : Type ι₂} {D₁ : Desc I₁ α₁} {D₂ : Desc I₂ α₂} {j₁ j₂}
-> ⟦ D₁ ≊ᵈ D₂ ⟧ -> ⟦ j₁ ≅ j₂ ⟧ -> μ D₁ j₁ -> μ D₂ j₂
coerceMu {α₁ = lzero } {lzero } qD qj d = proj₁ (qD _ _ qj) d
coerceMu {α₁ = lsuc _} {lsuc _} {D₁ = D₁} {D₂} qD qj (node e) =
node (coerceExtend D₁ D₂ qD (λ _ _ -> _,_ qD) qj e)
coerceMu {α₁ = lzero } {lsuc _} ()
coerceMu {α₁ = lsuc _} {lzero } ()
postulate
refl : ∀ {a} {α : Level a} {A : Univ α} -> (x : ⟦ A ⟧) -> ⟦ x ≅ x ⟧
coherence : ∀ {a b} {α : Level a} {β : Level b} {A : Univ α} {B : Univ β}
-> (q : ⟦ A ≈ B ⟧) -> (x : ⟦ A ⟧) -> ⟦ x ≅ coerce q x ⟧
cong-≅z : ∀ {a b c} {α : Level a} {β : Level b} {γ : Level c}
{A : Univ α} {B : Univ β} {C : Univ γ}
-> (x : ⟦ A ⟧) {y : ⟦ B ⟧} {z : ⟦ C ⟧} -> (q : ⟦ x ≅ y ⟧) -> ⟦ (x ≅ z) ≈ (y ≅ z)⟧
huip : ∀ {a b} {α : Level a} {β : Level b} {A : Univ α} {B : Univ β}
-> (x : ⟦ A ⟧) {y : ⟦ B ⟧} -> (q : ⟦ x ≅ y ⟧) -> ⟦ refl x ≅ q ⟧
right : ∀ {a b c} {α : Level a} {β : Level b} {γ : Level c}
{A : Univ α} {B : Univ β} {C : Univ γ}
-> (x : ⟦ A ⟧) {y : ⟦ B ⟧} {z : ⟦ C ⟧} -> ⟦ x ≅ y ⟧ -> ⟦ x ≅ z ⟧ -> ⟦ y ≅ z ⟧
right x q₁ = proj₁ (cong-≅z x q₁)
trans : ∀ {a b c} {α : Level a} {β : Level b} {γ : Level c}
{A : Univ α} {B : Univ β} {C : Univ γ}
-> (x : ⟦ A ⟧) {y : ⟦ B ⟧} {z : ⟦ C ⟧} -> ⟦ x ≅ y ⟧ -> ⟦ y ≅ z ⟧ -> ⟦ x ≅ z ⟧
trans x {y} q₁ = proj₂ (cong-≅z x q₁)
sym : ∀ {a b} {α : Level a} {β : Level b} {A : Univ α} {B : Univ β}
-> (x : ⟦ A ⟧) {y : ⟦ B ⟧} -> ⟦ x ≅ y ⟧ -> ⟦ y ≅ x ⟧
sym x q = right x q (refl x)
left : ∀ {a b c} {α : Level a} {β : Level b} {γ : Level c}
{A : Univ α} {B : Univ β} {C : Univ γ}
-> (x : ⟦ A ⟧) {y : ⟦ B ⟧} {z : ⟦ C ⟧} -> ⟦ x ≅ y ⟧ -> ⟦ z ≅ y ⟧ -> ⟦ x ≅ z ⟧
left x {z = z} q₁ q₂ = trans x q₁ (sym z q₂)
subst : ∀ {a b} {α : Level a} {β : Level b} {A : Univ α} {x y}
-> (B : ⟦ A ⟧ -> Univ β) -> ⟦ x ≅ y ⇒ B x ⇒ B y ⟧
subst B q = coerce (refl B _ _ q)
subst₂ : ∀ {a b c} {α : Level a} {β : Level b} {γ : Level c} {A : Univ α}
{B : ⟦ A ⟧ -> Univ β} {x₁ x₂} {y₁ : ⟦ B x₁ ⟧} {y₂ : ⟦ B x₂ ⟧}
-> (C : ∀ x -> ⟦ B x ⟧ -> Univ γ) -> ⟦ x₁ ≅ x₂ ⇒ y₁ ≅ y₂ ⇒ C x₁ y₁ ⇒ C x₂ y₂ ⟧
subst₂ C q₁ q₂ = coerce (refl C _ _ q₁ _ _ q₂)
J : ∀ {a b} {α : Level a} {β : Level b} {A : Univ α} {x y : ⟦ A ⟧}
-> (B : (y : ⟦ A ⟧) -> ⟦ x ≅ y ⟧ -> Univ β)
-> ⟦ B _ (refl x) ⟧
-> (q : ⟦ x ≅ y ⟧)
-> ⟦ B _ q ⟧
J {x = x} B z q = subst₂ B q (huip x q) z