-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathZS.agda
360 lines (273 loc) ยท 13.7 KB
/
ZS.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
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
{-# OPTIONS --cubical --guardedness --rewriting #-}
module ZS where
open import Agda.Primitive using (Level; lzero; lsuc; _โ_) public
open import Cubical.Core.Everything public
open import Cubical.Foundations.Everything renaming (cong to ap) public
open import Cubical.Data.Nat
open import Cubical.Data.Sigma
private
variable
โ โโ โโ โโ โโ : Level
{-# BUILTIN REWRITE _โก_ #-}
---------------------------------------------------------------------------
-- Type Structures
record TyStr โ : Type (lsuc โ) where
coinductive
field
๐ก๐ฆ : Type โ
๐๐ฅ : ๐ก๐ฆ โ TyStr โ
open TyStr public
record TyMor (๐ฏ : TyStr โโ) (๐ฎ : TyStr โโ) : Type (โโ โ โโ) where
coinductive
field
๐๐ข๐ : ๐ก๐ฆ ๐ฏ โ ๐ก๐ฆ ๐ฎ
๐ข๐ : (A : ๐ก๐ฆ ๐ฏ) โ TyMor (๐๐ฅ ๐ฏ A) (๐๐ฅ ๐ฎ (๐๐ข๐ A))
open TyMor public
idTyMor : (๐ฏ : TyStr โ) โ TyMor ๐ฏ ๐ฏ
๐๐ข๐ (idTyMor ๐ฏ) A = A
๐ข๐ (idTyMor ๐ฏ) A = idTyMor (๐๐ฅ ๐ฏ A)
infixl 20 _โTyMor_
_โTyMor_ : {๐ฏ : TyStr โโ} {๐ฎ : TyStr โโ} {โ : TyStr โโ} โ
TyMor ๐ฎ โ โ TyMor ๐ฏ ๐ฎ โ TyMor ๐ฏ โ
๐๐ข๐ (๐ โTyMor ๐) = ๐๐ข๐ ๐ โ ๐๐ข๐ ๐
๐ข๐ (๐ โTyMor ๐) A = ๐ข๐ ๐ (๐๐ข๐ ๐ A) โTyMor ๐ข๐ ๐ A
idR : {๐ฏโ : TyStr โโ} {๐ฏโ : TyStr โโ} (๐ : TyMor ๐ฏโ ๐ฏโ) โ
๐ โTyMor idTyMor ๐ฏโ โก ๐
๐๐ข๐ (idR ๐ i) A = ๐๐ข๐ ๐ A
๐ข๐ (idR ๐ i) A = idR (๐ข๐ ๐ A) i
{-# REWRITE idR #-}
---------------------------------------------------------------------------
-- Wk, Z, and S Structures
record WkStr (๐ฏ : TyStr โ) : Type โ where
coinductive
field
๐ค๐ : (A : ๐ก๐ฆ ๐ฏ) โ TyMor ๐ฏ (๐๐ฅ ๐ฏ A)
๐๐ฅ : (A : ๐ก๐ฆ ๐ฏ) โ WkStr (๐๐ฅ ๐ฏ A)
open WkStr
record ZStr (๐ฏ : TyStr โโ) โโ : Type (โโ โ (lsuc โโ)) where
coinductive
field
๐ก๐ฆแถป : ๐ก๐ฆ ๐ฏ โ Type โโ
๐๐ฅแถป : {A : ๐ก๐ฆ ๐ฏ} (A' : ๐ก๐ฆแถป A) โ ZStr (๐๐ฅ ๐ฏ A) โโ
open ZStr
-- a SStr is a morphism of dependent TyStrs from Z to EX
record SStr {๐ฏโ : TyStr โโ} {๐ฏโ : TyStr โโ} (๐ : TyMor ๐ฏโ ๐ฏโ)
(Z : ZStr ๐ฏโ โโ) (๐ฒ : WkStr ๐ฏโ) : Type (โโ โ โโ โ โโ) where
coinductive
field
๐๐ข๐หข : {A : ๐ก๐ฆ ๐ฏโ} (๐ : ๐ก๐ฆแถป Z A) โ ๐ก๐ฆ (๐๐ฅ ๐ฏโ (๐๐ข๐ ๐ A))
๐ข๐หข : {A : ๐ก๐ฆ ๐ฏโ} (๐ : ๐ก๐ฆแถป Z A) โ
SStr (๐ค๐ (๐๐ฅ ๐ฒ (๐๐ข๐ ๐ A)) (๐๐ข๐หข ๐) โTyMor ๐ข๐ ๐ A)
(๐๐ฅแถป Z ๐) (๐๐ฅ (๐๐ฅ ๐ฒ (๐๐ข๐ ๐ A)) (๐๐ข๐หข ๐))
open SStr
---------------------------------------------------------------------------
-- Contexts
data ๐ถ๐ก๐ฅ (๐ฏ : TyStr โ) : โ โ Type โ
๐๐ฅ๐ : (๐ฏ : TyStr โ) {n : โ} โ ๐ถ๐ก๐ฅ ๐ฏ n โ TyStr โ
infixl 20 _โน_
data ๐ถ๐ก๐ฅ ๐ฏ where
โ
: ๐ถ๐ก๐ฅ ๐ฏ 0
_โน_ : {n : โ} (ฮ : ๐ถ๐ก๐ฅ ๐ฏ n) โ ๐ก๐ฆ (๐๐ฅ๐ ๐ฏ ฮ) โ ๐ถ๐ก๐ฅ ๐ฏ (suc n)
ฯ๐ถ๐ก๐ฅ : {๐ฏ : TyStr โ} {n : โ} โ ๐ถ๐ก๐ฅ ๐ฏ (suc n) โ ๐ถ๐ก๐ฅ ๐ฏ n
ฯ๐ถ๐ก๐ฅ (ฮ โน A) = ฮ
๐ง๐ถ๐ก๐ฅ : {๐ฏ : TyStr โ} {n : โ} (ฮ : ๐ถ๐ก๐ฅ ๐ฏ (suc n)) โ ๐ก๐ฆ (๐๐ฅ๐ ๐ฏ (ฯ๐ถ๐ก๐ฅ ฮ))
๐ง๐ถ๐ก๐ฅ (ฮ โน A) = A
๐๐ฅ๐ ๐ฏ {n = 0} ฮ = ๐ฏ
๐๐ฅ๐ ๐ฏ {n = suc n} ฮ = ๐๐ฅ (๐๐ฅ๐ ๐ฏ (ฯ๐ถ๐ก๐ฅ ฮ)) (๐ง๐ถ๐ก๐ฅ ฮ)
๐ฒ-๐๐ฅ๐ : {๐ฏ : TyStr โโ} (๐ฒ : WkStr ๐ฏ) {n : โ} (ฮ : ๐ถ๐ก๐ฅ ๐ฏ n) โ
WkStr (๐๐ฅ๐ ๐ฏ ฮ)
๐ฒ-๐๐ฅ๐ ๐ฒ {n = zero} ฮ = ๐ฒ
๐ฒ-๐๐ฅ๐ ๐ฒ {n = suc n} ฮ = ๐๐ฅ (๐ฒ-๐๐ฅ๐ ๐ฒ (ฯ๐ถ๐ก๐ฅ ฮ)) (๐ง๐ถ๐ก๐ฅ ฮ)
data ๐ถ๐ก๐ฅแถป {๐ฏ : TyStr โโ} (๐ฎ : ZStr ๐ฏ โโ)
: {n : โ} โ ๐ถ๐ก๐ฅ ๐ฏ n โ Type (โโ โ โโ)
๐๐ฅ๐ แถป : {๐ฏ : TyStr โโ} (๐ฎ : ZStr ๐ฏ โโ) {n : โ} {ฮ : ๐ถ๐ก๐ฅ ๐ฏ n} โ
๐ถ๐ก๐ฅแถป ๐ฎ ฮ โ ZStr (๐๐ฅ๐ ๐ฏ ฮ) โโ
data ๐ถ๐ก๐ฅแถป {๐ฏ = ๐ฏ} ๐ฎ where
โ
: {ฮ : ๐ถ๐ก๐ฅ ๐ฏ 0} โ ๐ถ๐ก๐ฅแถป ๐ฎ ฮ
_โน_ : {n : โ} {ฮ : ๐ถ๐ก๐ฅ ๐ฏ (suc n)}
(ฮ' : ๐ถ๐ก๐ฅแถป ๐ฎ (ฯ๐ถ๐ก๐ฅ ฮ)) โ ๐ก๐ฆแถป (๐๐ฅ๐ แถป ๐ฎ ฮ') (๐ง๐ถ๐ก๐ฅ ฮ) โ ๐ถ๐ก๐ฅแถป ๐ฎ ฮ
ฯ๐ถ๐ก๐ฅแถป : {๐ฏ : TyStr โโ} {๐ฎ : ZStr ๐ฏ โโ} {n : โ} {ฮ : ๐ถ๐ก๐ฅ ๐ฏ (suc n)} โ
๐ถ๐ก๐ฅแถป ๐ฎ ฮ โ ๐ถ๐ก๐ฅแถป ๐ฎ (ฯ๐ถ๐ก๐ฅ ฮ)
ฯ๐ถ๐ก๐ฅแถป (ฮ' โน A') = ฮ'
๐ง๐ถ๐ก๐ฅแถป : {๐ฏ : TyStr โโ} {๐ฎ : ZStr ๐ฏ โโ} {n : โ} {ฮ : ๐ถ๐ก๐ฅ ๐ฏ (suc n)} โ
(ฮ' : ๐ถ๐ก๐ฅแถป ๐ฎ ฮ) โ ๐ก๐ฆแถป (๐๐ฅ๐ แถป ๐ฎ (ฯ๐ถ๐ก๐ฅแถป ฮ')) (๐ง๐ถ๐ก๐ฅ ฮ)
๐ง๐ถ๐ก๐ฅแถป (ฮ' โน A') = A'
๐๐ฅ๐ แถป ๐ฎ {n = 0} ฮ' = ๐ฎ
๐๐ฅ๐ แถป ๐ฎ {n = suc n} ฮ' = ๐๐ฅแถป (๐๐ฅ๐ แถป ๐ฎ (ฯ๐ถ๐ก๐ฅแถป ฮ')) (๐ง๐ถ๐ก๐ฅแถป ฮ')
double : โ โ โ
double zero = zero
double (suc n) = suc (suc (double n))
-- produces a context in ๐ฏ from a Z-section of ๐ธ๐ ๐ฏ
๐๐๐๐ก : {๐ฏโ : TyStr โโ} {๐ฏโ : TyStr โโ} {๐ : TyMor ๐ฏโ ๐ฏโ}
{Z : ZStr ๐ฏโ โโ} {๐ฒ : WkStr ๐ฏโ} (๐ฎ : SStr ๐ Z ๐ฒ)
{n : โ} {ฮ : ๐ถ๐ก๐ฅ ๐ฏโ n} (๐s : ๐ถ๐ก๐ฅแถป Z ฮ) โ ๐ถ๐ก๐ฅ ๐ฏโ (double n)
๐๐๐ : {๐ฏโ : TyStr โโ} {๐ฏโ : TyStr โโ} {๐ : TyMor ๐ฏโ ๐ฏโ}
{Z : ZStr ๐ฏโ โโ} {๐ฒ : WkStr ๐ฏโ} (๐ฎ : SStr ๐ Z ๐ฒ)
{n : โ} {ฮ : ๐ถ๐ก๐ฅ ๐ฏโ n} (๐s : ๐ถ๐ก๐ฅแถป Z ฮ) โ
TyMor (๐๐ฅ๐ ๐ฏโ ฮ) (๐๐ฅ๐ ๐ฏโ (๐๐๐๐ก ๐ฎ ๐s))
๐ข๐๐ หข : {๐ฏโ : TyStr โโ} {๐ฏโ : TyStr โโ} {๐ : TyMor ๐ฏโ ๐ฏโ}
{Z : ZStr ๐ฏโ โโ} {๐ฒ : WkStr ๐ฏโ} (๐ฎ : SStr ๐ Z ๐ฒ)
{n : โ} {ฮ : ๐ถ๐ก๐ฅ ๐ฏโ n} (๐s : ๐ถ๐ก๐ฅแถป Z ฮ) โ
SStr (๐๐๐ ๐ฎ ๐s) (๐๐ฅ๐ แถป Z ๐s) (๐ฒ-๐๐ฅ๐ ๐ฒ (๐๐๐๐ก ๐ฎ ๐s))
๐๐๐๐ก ๐ฎ โ
= โ
๐๐๐๐ก {๐ = ๐} ๐ฎ {ฮ = ฮ โน A} (๐s โน ๐) =
๐๐๐๐ก ๐ฎ ๐s โน ๐๐ข๐ (๐๐๐ ๐ฎ ๐s) A โน ๐๐ข๐หข (๐ข๐๐ หข ๐ฎ ๐s) ๐
๐๐๐ {๐ = ๐} ๐ฎ โ
= ๐
๐๐๐ {๐ฒ = ๐ฒ} ๐ฎ {ฮ = ฮ โน A} (๐s โน ๐) =
๐ค๐ (๐๐ฅ (๐ฒ-๐๐ฅ๐ ๐ฒ (๐๐๐๐ก ๐ฎ ๐s)) (๐๐ข๐ (๐๐๐ ๐ฎ ๐s) A)) (๐๐ข๐หข (๐ข๐๐ หข ๐ฎ ๐s) ๐)
โTyMor ๐ข๐ (๐๐๐ ๐ฎ ๐s) A
๐ข๐๐ หข ๐ฎ โ
= ๐ฎ
๐ข๐๐ หข ๐ฎ {ฮ = ฮ โน A} (๐s โน ๐) = ๐ข๐หข (๐ข๐๐ หข ๐ฎ ๐s) ๐
---------------------------------------------------------------------------
-- Indexing
data Fin : โ โ Type where
๐ : {n : โ} โ Fin n
๐ : {n : โ} โ Fin n โ Fin (suc n)
split : (n m : โ) โ Fin (m + n)
split n zero = ๐
split n (suc m) = ๐ (split n m)
full : (n : โ) โ Fin n
full zero = ๐
full (suc n) = ๐ (full n)
sub : (n : โ) โ Fin n โ โ
sub n ๐ = n
sub (suc n) (๐ m) = sub n m
shift : {n : โ} โ Fin n โ Fin (suc n)
shift ๐ = ๐
shift (๐ m) = ๐ (shift m)
sub-split : (n m : โ) โ sub (m + n) (split n m) โก n
sub-split n zero = refl
sub-split n (suc m) = sub-split n m
sub-full : (n : โ) โ sub n (full n) โก zero
sub-full zero = refl
sub-full (suc n) = sub-full n
sub-shift : {n : โ} (m : Fin n) โ sub (suc n) (shift m) โก suc (sub n m)
sub-shift ๐ = refl
sub-shift (๐ m) = sub-shift m
{-# REWRITE sub-split sub-full sub-shift #-}
drop : {๐ฏ : TyStr โ} {n : โ} (ฮ : ๐ถ๐ก๐ฅ ๐ฏ n) (m : Fin n) โ ๐ถ๐ก๐ฅ ๐ฏ (sub n m)
drop ฮ ๐ = ฮ
drop ฮ (๐ m) = drop (ฯ๐ถ๐ก๐ฅ ฮ) m
index : {๐ฏ : TyStr โ} {n : โ} (ฮ : ๐ถ๐ก๐ฅ ๐ฏ (suc n)) (m : Fin n) โ
๐ก๐ฆ (๐๐ฅ๐ ๐ฏ (drop ฮ (๐ m)))
index ฮ ๐ = ๐ง๐ถ๐ก๐ฅ ฮ
index ฮ (๐ m) = index (ฯ๐ถ๐ก๐ฅ ฮ) m
drop-full : {๐ฏ : TyStr โ} {n : โ} (ฮ : ๐ถ๐ก๐ฅ ๐ฏ n) โ
drop ฮ (full n) โก โ
drop-full โ
= refl
drop-full (ฮ โน A) = drop-full ฮ
index-lem : {๐ฏ : TyStr โ} {n : โ} (ฮ : ๐ถ๐ก๐ฅ ๐ฏ (suc n)) (m : Fin n) โ
drop ฮ (shift m) โก drop (ฯ๐ถ๐ก๐ฅ ฮ) m โน index ฮ m
index-lem (ฮ โน A) ๐ = refl
index-lem (ฮ โน A) (๐ m) = index-lem ฮ m
{-# REWRITE drop-full index-lem #-}
---------------------------------------------------------------------------
-- SSTs
-- this solves the problem of simplex extraction
module _ {๐ฏ : TyStr โโ} {๐ฒ : WkStr ๐ฏ} {Z : ZStr ๐ฏ โโ}
(S : SStr (idTyMor ๐ฏ) Z ๐ฒ) where
record State : Type (โโ โ โโ) where
constructor state
field
n : โ
ฮ : ๐ถ๐ก๐ฅ ๐ฏ (suc n)
m : Fin (suc n)
๐s : ๐ถ๐ก๐ฅแถป Z (drop ฮ m)
promote : State โ State
promote (state n ฮ ๐ ๐s) =
state (suc (double n)) (๐๐๐๐ก S ๐s) (full (double (suc n))) โ
promote (state n ฮ (๐ m) ๐s) = state n ฮ (๐ m) ๐s
length : State โ โ
length (state n ฮ ๐ ๐s) = length (promote (state n ฮ ๐ ๐s))
length (state n ฮ (๐ m) ๐s) = sub n m
context : (๐ฎ : State) โ ๐ถ๐ก๐ฅ ๐ฏ (length ๐ฎ)
context (state n ฮ ๐ ๐s) = context (promote (state n ฮ ๐ ๐s))
context (state n ฮ (๐ m) ๐s) = drop ฮ (๐ m)
Z-context : (๐ฎ : State) โ ๐ถ๐ก๐ฅแถป Z (context ๐ฎ)
Z-context (state n ฮ ๐ ๐s) = Z-context (promote (state n ฮ ๐ ๐s))
Z-context (state n ฮ (๐ m) ๐s) = ๐s
type : (๐ฎ : State) โ ๐ก๐ฆ (๐๐ฅ๐ ๐ฏ (context ๐ฎ))
type (state n ฮ ๐ ๐s) = type (promote (state n ฮ ๐ ๐s))
type (state n ฮ (๐ m) ๐s) = index ฮ m
Req : State โ Type โโ
Req ๐ฎ = ๐ก๐ฆแถป (๐๐ฅ๐ แถป Z (Z-context ๐ฎ)) (type ๐ฎ)
ex : (๐ ๐ก๐๐ก๐ : State) โ Req ๐ ๐ก๐๐ก๐ โ State
ex (state n ฮ ๐ ๐s) ๐ =
state (suc (double n)) (๐๐๐๐ก S ๐s)
(shift (full (suc (double n)))) (โ
โน ๐)
ex (state n ฮ (๐ m) ๐s) ๐ = state n ฮ (shift m) (๐s โน ๐)
ฮ' : State โ TyStr โโ
๐ก๐ฆ (ฮ' ๐ ๐ก๐๐ก๐) = Req ๐ ๐ก๐๐ก๐
๐๐ฅ (ฮ' ๐ ๐ก๐๐ก๐) ๐ = ฮ' (ex ๐ ๐ก๐๐ก๐ ๐)
ฮ : {n : โ} (ฮ : ๐ถ๐ก๐ฅ ๐ฏ (suc n)) โ TyStr โโ
ฮ {n = n} ฮ = ฮ' (state n ฮ (full (suc n)) โ
)
---------------------------------------------------------------------------
-- Sing
๐ฐ' : (X : Type โ) โ TyStr (lsuc โ)
๐ก๐ฆ (๐ฐ' {โ} X) = X โ Type โ
๐๐ฅ (๐ฐ' X) A = ๐ฐ' (ฮฃ X A)
๐ฐ : (โ : Level) โ TyStr (lsuc โ)
๐ก๐ฆ (๐ฐ โ) = Type โ
๐๐ฅ (๐ฐ โ) A = ๐ฐ' A
replace : {X Y : Type โ} (f : X โ Y) โ TyMor (๐ฐ' Y) (๐ฐ' X)
๐๐ข๐ (replace f) A = A โ f
๐ข๐ (replace f) A = replace (ฮป x โ f (fst x) , snd x)
replaceยฒ : {X Y Z : Type โ} (f : X โ Y) (g : Y โ Z) โ
replace f โTyMor replace g โก replace (g โ f)
๐๐ข๐ (replaceยฒ f g i) A x = A (g (f x))
๐ข๐ (replaceยฒ f g i) A =
replaceยฒ (ฮป x โ f (fst x) , snd x) (ฮป y โ g (fst y) , snd y) i
{-# REWRITE replaceยฒ #-}
๐ฒ-๐ฐ' : (X : Type โ) โ WkStr (๐ฐ' X)
๐ค๐ (๐ฒ-๐ฐ' X) A = replace fst
๐๐ฅ (๐ฒ-๐ฐ' X) A = ๐ฒ-๐ฐ' (ฮฃ X A)
๐ฒ-๐ฐ : WkStr (๐ฐ โ)
๐๐ข๐ (๐ค๐ ๐ฒ-๐ฐ A) B = ฮป _ โ B
๐ข๐ (๐ค๐ ๐ฒ-๐ฐ A) B = replace snd
๐๐ฅ ๐ฒ-๐ฐ A = ๐ฒ-๐ฐ' A
Z' : {X : Type โ} โ X โ ZStr (๐ฐ' X) โ
๐ก๐ฆแถป (Z' x) A = A x
๐๐ฅแถป (Z' x) a = Z' (x , a)
Z : ZStr (๐ฐ โ) โ
๐ก๐ฆแถป Z A = A
๐๐ฅแถป Z a = Z' a
S' : {X Y : Type โ} (f : X โ Y) (y : Y) (p : (x : X) โ y โก f x) โ
SStr (replace f) (Z' y) (๐ฒ-๐ฐ' X)
๐๐ข๐หข (S' f y p) {A} aโ = ฮป {(x , aโ) โ PathP (ฮป i โ A (p x i)) aโ aโ}
๐ข๐หข (S' f y p) {A} a =
S' (ฮป x โ f (fst (fst x)) , snd (fst x)) (y , a)
(ฮป x i โ p (fst (fst x)) i , snd x i)
S : SStr (idTyMor (๐ฐ โ)) Z ๐ฒ-๐ฐ
๐๐ข๐หข S aโ aโ = aโ โก aโ
๐ข๐หข S a = S' fst a snd
Sing : (X : Type โ) โ TyStr โ
Sing X = ฮ S (โ
โน X)
-- here is the result of applying the simplex extraction algorithm to Sing
-- the following fields were produced by starting with:
-- ๐ก๐ฆ (๐๐ฅ๐ (Sing X) โ
) = ๐ก๐ฆ (Sing X) = X
-- then we take x : X, and add that to the empty context; we have:
-- ๐ก๐ฆ (๐๐ฅ๐ (Sing X) (โ
โน x)) = X
-- so we take y : X, and then see that:
-- ๐ก๐ฆ (๐๐ฅ๐ (Sing X) (โ
โน x โน y)) = x โก y
-- we repeat until we fill in a 3-simplex
-- the well-formed-context entry shows that the extracted types are right!
record 3-simplex (X : Type) : Type where
field
x : X
y : X
ฮฑ : x โก y
z : X
ฮฒ : y โก z
ฮณ : x โก z
๐โ : PathP (ฮป i โ x โก ฮฒ i) ฮฑ ฮณ
w : X
ฮด : z โก w
ฮต : y โก w
๐โ : PathP (ฮป i โ y โก ฮด i) ฮฒ ฮต
ฮถ : x โก w
๐โ : PathP (ฮป i โ x โก ฮด i) ฮณ ฮถ
๐โ : PathP (ฮป i โ x โก ฮต i) ฮฑ ฮถ
ฮโ : PathP (ฮป i โ PathP (ฮป j โ x โก ๐โ i j) ฮฑ (๐โ i)) ๐โ ๐โ
well-formed-context : ๐ถ๐ก๐ฅ (Sing X) 15
well-formed-context =
โ
โน x โน y โน ฮฑ โน z โน ฮฒ โน ฮณ โน ๐โ โน w โน ฮด โน ฮต โน ๐โ โน ฮถ โน ๐โ โน ๐โ โน ฮโ