-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathopetope.html
486 lines (350 loc) · 25.2 KB
/
opetope.html
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
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
<!DOCTYPE html>
<html>
<head>
<meta charset='utf-8'>
<meta name='duration' content='60' />
<link href="https://github.global.ssl.fastly.net/assets/github-1cddff501e45a3bd3dd9bd109289016b0a6f5078.css" media="all" rel="stylesheet" type="text/css" />
<link href="https://github.global.ssl.fastly.net/assets/github2-f7d3949d521522afe3043f63bd1e1a86e82221d1.css" media="all" rel="stylesheet" type="text/css" />
<script src="https://github.global.ssl.fastly.net/assets/frameworks-5970f5a0a3dcc441d5f7ff74326ffd59bbe9388e.js" type="text/javascript"></script>
<script src="https://github.global.ssl.fastly.net/assets/github-00445d3177bccff81702c1d3fc3aaef72a724a5a.js" type="text/javascript"></script>
<title>Seminar — Opetopes</title>
<meta name='copyright'
content='Copyright © 2013 Gabor Greif' />
<link rel='stylesheet' type='text/css' media='screen, projection, print'
href='https://www.w3.org/Talks/Tools/Slidy2/styles/slidy.css' />
<script src='https://www.w3.org/Talks/Tools/Slidy2/scripts/slidy.js'
charset='utf-8' type='text/javascript'></script>
<style type='text/css'>
div.slide h1 {
font-size: 2.5em;
}
</style>
</head>
<body>
<div class='slide markdown-body'><h1>
<a name="short-intro-to-opetopes" class="anchor" href="#short-intro-to-opetopes"></a>Short Intro to Opetopes</h1>
<p>Seminar 2013-11-19</p>
<p>My goals:</p>
<ol>
<li>form an intuition of opetopic sets</li>
<li>sketch a calculus of (string) diagrams</li>
<li>discuss the missing piece of cartesian closure</li>
<li>potential applications to Ωmega 2.0</li>
</ol></div>
<div class='slide markdown-body'><h1>
<a name="origin" class="anchor" href="#origin"></a>Origin</h1>
<p>Mid-1990'es by Baez and Dolan (<em>metatree</em>, <em>opetope</em>), published as <a href="http://arxiv.org/pdf/q-alg/9702014.pdf">arXiv:q-alg/9702014</a>.</p>
<p>TQFTs <a href="http://arxiv.org/pdf/q-alg/9503002.pdf">arXiv:q-alg/9503002</a></p>
</div>
<div class='slide markdown-body'><h1>
<a name="many-people" class="anchor" href="#many-people"></a>Many People</h1>
<p>Various researchers/groups contributed since, and similar concepts go by a multitude of names</p>
<ul>
<li>Multitopes – Hermida, Makkai</li>
<li>Opetopes – Eugenia Cheng (e.g. <a href="http://arxiv.org/pdf/math/0304284.pdf">arXiv:math/0304284</a>)</li>
<li>"positive-to-one computads" – Marek Zawadowski, <a href="http://arxiv.org/pdf/0708.2658.pdf">arXiv:0708.2658</a>
</li>
<li>Szawiel, Marek Zawadowski <a href="http://arxiv.org/pdf/1011.2374.pdf">arXiv:1011.2374</a>
</li>
<li>Joachim Kock, <em>et al</em>. <a href="http://arxiv.org/pdf/0706.1033.pdf">arXiv:0706.1033</a>
</li>
</ul><p>At IAS:</p>
<ul>
<li>Krzysztof Kapulkin</li>
<li>Eric Finster</li>
</ul></div>
<div class='slide markdown-body'><h1>
<a name="higher-dimensional-trees" class="anchor" href="#higher-dimensional-trees"></a>Higher-dimensional Trees</h1>
<p>Polynomial functors and monads (iterated construction)</p>
</div>
<div class='slide markdown-body'><h1>
<a name="zooms-and-complexes" class="anchor" href="#zooms-and-complexes"></a>Zooms and Complexes</h1>
<p>We define <em>zooms</em> as configurable 'tree transformers'.</p>
<p>Then we compose zooms to compexes, subject to boundary conditions.</p>
</div>
<div class='slide markdown-body'><h2>
<a name="zoom-definition" class="anchor" href="#zoom-definition"></a>Zoom definition</h2>
<p><a href="https://rawgithub.com/ggreif/seminar-opetope/master/zoom.svg" target="_blank"><img src="https://rawgithub.com/ggreif/seminar-opetope/master/zoom.svg" alt="A typical zoom" style="max-width:100%;"></a></p>
<p>Input data: finite rooted (planar) trees (the nth dimension)</p>
<p>Freely decorate with disks, adhering to rules:</p>
<ul>
<li>disk must cut branch(es), but nothing else</li>
<li>every disk must capture a subtree</li>
</ul></div>
<div class='slide markdown-body'><h2>
<a name="input-to-output-translation" class="anchor" href="#input-to-output-translation"></a>Input-to-output translation</h2>
<p><a href="https://github.com/ggreif/seminar-opetope/blob/master/opetope2.stl">Just change the perspective!</a></p>
<p>Translate to tree in the (n+1)th dimension</p>
<table>
<thead><tr>
<th align="right">Input</th>
<th align="center"></th>
<th align="left">Output</th>
</tr></thead>
<tbody>
<tr>
<td align="right">branch</td>
<td align="center">⊣</td>
<td align="left"></td>
</tr>
<tr>
<td align="right">dot</td>
<td align="center">⇒</td>
<td align="left">(unit) branch</td>
</tr>
<tr>
<td align="right">disk</td>
<td align="center">⇒</td>
<td align="left">dot</td>
</tr>
</tbody>
</table></div>
<div class='slide markdown-body'><h2>
<a name="special-case-corolla" class="anchor" href="#special-case-corolla"></a>Special case: <em>corolla</em>
</h2>
<p>A <em>corolla</em> is a special zoom with just one dot in the left tree and no disks.</p>
<p><a href="https://rawgithub.com/ggreif/seminar-opetope/master/corolla.svg" target="_blank"><img src="https://rawgithub.com/ggreif/seminar-opetope/master/corolla.svg" alt="A corolla" style="max-width:100%;"></a></p>
<p>The output tree is thus a <em>unit branch</em>:</p>
<p><a href="https://rawgithub.com/ggreif/seminar-opetope/master/corolla-zoom.svg" target="_blank"><img src="https://rawgithub.com/ggreif/seminar-opetope/master/corolla-zoom.svg" alt="Corolla in zoom view" style="max-width:100%;"></a></p>
</div>
<div class='slide markdown-body'><h2>
<a name="assembling-the-complex" class="anchor" href="#assembling-the-complex"></a>Assembling the complex</h2>
<p>The trees have labelled branches and dots (without repetition)</p>
<p><a href="https://rawgithub.com/ggreif/seminar-opetope/master/labelled-zoom.svg" target="_blank"><img src="https://rawgithub.com/ggreif/seminar-opetope/master/labelled-zoom.svg" alt="Labelled zoom" style="max-width:100%;"></a></p>
<p>Zooms can be joined when the trees match, forming a <em>zoom complex</em>.</p>
<p><a href="https://rawgithub.com/ggreif/seminar-opetope/master/zoom-complex.svg" target="_blank"><img src="https://rawgithub.com/ggreif/seminar-opetope/master/zoom-complex.svg" alt="Formed complex" style="max-width:100%;"></a></p>
<p><em>Note:</em> These complexes form a <a href="http://ncatlab.org/nlab/show/semicategory">semicategory</a>,
as there are input trees not admitting an identity zoom (e.g. unit tree, most corollas).</p>
</div>
<div class='slide markdown-body'><h2>
<a name="opetope" class="anchor" href="#opetope"></a>Opetope</h2>
<p>A zoom complex with dimensions</p>
<table>
<thead><tr>
<th align="right">-2</th>
<th align="center">-1</th>
<th>…</th>
<th align="left"><em>n+1</em></th>
</tr></thead>
<tbody><tr>
<td align="right">O</td>
<td align="center">(.)</td>
<td></td>
<td align="left">.</td>
</tr></tbody>
</table><p>and a <em>corolla</em> appearing in the last dimension
is called an <em>opetope</em>.</p>
<p>Opetopes are normally drawn starting with dimension 0.</p>
<ul>
<li>a 0-dimensional opetope is (isomorphic to) a natural number</li>
<li>the zoom in dimension 1 has a planar tree input</li>
</ul><p><a href="http://sma.epfl.ch/%7Efinster/opetope/opetope.html">You can construct opetopes interactively.</a></p>
</div>
<div class='slide markdown-body'><h1>
<a name="inductive-datatypes" class="anchor" href="#inductive-datatypes"></a>Inductive Datatypes</h1>
<p>Finster gives <a href="http://sma.epfl.ch/%7Efinster/opetope/types-and-opetopes.pdf#page=26">data type</a> + <em>typechecker</em></p>
<p>But <a href="http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus#Intrinsic_vs._extrinsic_interpretations">intrinsic definition</a>
of <code>Zoom</code>s <a href="https://code.google.com/p/omega/source/browse/trunk/tests/Opetope.prg">is possible</a>.</p>
</div>
<div class='slide markdown-body'><h1>
<a name="category-of-opetopes" class="anchor" href="#category-of-opetopes"></a>Category of Opetopes</h1>
<p>Similarly defined as the category of singular complexes ∆</p>
<ul>
<li><p>Morphisms are face maps (corresponding to each 'round-ish thing')</p></li>
<li><p>Identity morphism (the top cell)</p></li>
</ul></div>
<div class='slide markdown-body'><h2>
<a name="pointers" class="anchor" href="#pointers"></a>Pointers</h2>
<p>To <em>mark</em> (e.g.) a dot in a tree we use trees that only have one unit branch</p>
<p><a href="https://rawgithub.com/ggreif/seminar-opetope/master/pointer.svg" target="_blank"><img src="https://rawgithub.com/ggreif/seminar-opetope/master/pointer.svg" alt="A pointer" style="max-width:100%;"></a></p>
</div>
<div class='slide markdown-body'><h2>
<a name="composition" class="anchor" href="#composition"></a>Composition</h2>
<p>"pointer" tree to mark a unit branch</p>
<p>then graft</p>
</div>
<div class='slide markdown-body'><h2>
<a name="substitution" class="anchor" href="#substitution"></a>Substitution</h2>
<p>Mark an n-ary node (or disk), swap it for an n-ary tree</p>
<p><a href="https://rawgithub.com/ggreif/seminar-opetope/master/substitution.svg" target="_blank"><img src="https://rawgithub.com/ggreif/seminar-opetope/master/substitution.svg" alt="Substitute" style="max-width:100%;"></a></p>
<p>Analogous to monadic <em>bind</em>.</p>
</div>
<div class='slide markdown-body'><h1>
<a name="geometric-realization" class="anchor" href="#geometric-realization"></a>Geometric Realization</h1>
<p>As <em>pasting diagrams</em>.</p>
<p><a href="https://rawgithub.com/ggreif/seminar-opetope/master/pasting-diagram.svg" target="_blank"><img src="https://rawgithub.com/ggreif/seminar-opetope/master/pasting-diagram.svg" alt="Pasting diagram" style="max-width:100%;"></a></p>
<p><a href="http://www-bcf.usc.edu/%7Elauda/xy/stringtutorial">As <em>string diagrams</em></a> (dual to the above).</p>
</div>
<div class='slide markdown-body'><h1>
<a name="coherence-conditions" class="anchor" href="#coherence-conditions"></a>Coherence conditions</h1>
<p>Automatically "type-checked"</p>
</div>
<div class='slide markdown-body'><h1>
<a name="deductions-following-finster" class="anchor" href="#deductions-following-finster"></a>Deductions (following Finster)</h1>
<p>Let's have a <em>formal language</em> whose 'terms' are pasting diagrams.</p>
<p>We (say) start out with a set of basic opetopes (<em>axioms</em>).</p>
<p>What are the <em>deduction rules</em> to create new ones?</p>
<p><a href="https://github-camo.global.ssl.fastly.net/60190af05a818dc83079f4c9b561e6bdc9d5cbe3/687474703a2f2f6c617465782e636f6465636f67732e636f6d2f7376672e6c617465783f5c6d61746862667b5365747d5e5c6d61746863616c7b4f7d5c72696768746172726f775c6d61746862667b4361747d5e5c6d61746863616c7b4f7d" target="_blank"><img src="https://github-camo.global.ssl.fastly.net/60190af05a818dc83079f4c9b561e6bdc9d5cbe3/687474703a2f2f6c617465782e636f6465636f67732e636f6d2f7376672e6c617465783f5c6d61746862667b5365747d5e5c6d61746863616c7b4f7d5c72696768746172726f775c6d61746862667b4361747d5e5c6d61746863616c7b4f7d" border="0" style="max-width:100%;"></a></p>
</div>
<div class='slide markdown-body'><h2>
<a name="empty-rule" class="anchor" href="#empty-rule"></a>Empty rule</h2>
<p>From any opetope one can derive an empty pasting diagram one dimension up.</p>
<p><a href="#special-case-corolla">See the corolla zoom</a>. It only shows the highest-dimensional
zoom, but that is ok as nothing below changes.</p>
</div>
<div class='slide markdown-body'><h2>
<a name="paste-rule" class="anchor" href="#paste-rule"></a>Paste rule</h2>
<p>Given <em>n</em> pasting diagrams and a cell (corolla) with <em>n</em> branches</p>
<ul>
<li>such that the target cells of the pasting diagrams match the (input) branches</li>
<li>then a bigger pasting diagram can be created</li>
</ul><p><a href="#composition">See pointer guided composition</a>, which is the atomic operation underlying this rule.</p>
</div>
<div class='slide markdown-body'><h2>
<a name="composite-rule" class="anchor" href="#composite-rule"></a>Composite rule</h2>
</div>
<div class='slide markdown-body'><h2>
<a name="universal-cell-introduction" class="anchor" href="#universal-cell-introduction"></a>Universal cell introduction</h2>
</div>
<div class='slide markdown-body'><h2>
<a name="universal-cell-elimination" class="anchor" href="#universal-cell-elimination"></a>Universal cell elimination</h2>
<p>Similar to the <a href="http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/">J-rule</a></p>
<p><a href="https://github-camo.global.ssl.fastly.net/cf1e1e9f24c2aa2b4a104441055dd725136def29/687474703a2f2f696d616765732e616d617a6f6e2e636f6d2f696d616765732f472f30312f6476642f63696e646572656c6c612d70756d706b696e2d6c617267652e6a7067" target="_blank"><img src="https://github-camo.global.ssl.fastly.net/cf1e1e9f24c2aa2b4a104441055dd725136def29/687474703a2f2f696d616765732e616d617a6f6e2e636f6d2f696d616765732f472f30312f6476642f63696e646572656c6c612d70756d706b696e2d6c617267652e6a7067" alt="The power of the universal cell" style="max-width:100%;"></a></p>
</div>
<div class='slide markdown-body'><h1>
<a name="can-we-obtain-cartesian-closure" class="anchor" href="#can-we-obtain-cartesian-closure"></a>Can we Obtain Cartesian Closure?</h1>
<p>Tensor product on operads <a href="http://arxiv.org/pdf/math/0701293.pdf">http://arxiv.org/pdf/math/0701293.pdf</a></p>
<p>Boardman-Vogt tensoring: <a href="http://arxiv.org/pdf/1302.3711.pdf">http://arxiv.org/pdf/1302.3711.pdf</a></p>
<p>Operator categories: <a href="http://arxiv.org/pdf/1302.5756.pdf">http://arxiv.org/pdf/1302.5756.pdf</a></p>
<p>Symmetric monoidal closed, yes, but cartesian?</p>
<ul>
<li>Gambino and Joyal: <a href="http://www1.maths.leeds.ac.uk/%7Epmtng/Research/Lectures/gambino-bmc.pdf">http://www1.maths.leeds.ac.uk/~pmtng/Research/Lectures/gambino-bmc.pdf</a>
</li>
</ul></div>
<div class='slide markdown-body'><h1>
<a name="excursion-lambda-calculus" class="anchor" href="#excursion-lambda-calculus"></a>Excursion: Lambda Calculus</h1>
<p>Several notations, e.g. λ (with μ), <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.6554">item notation (Kamareddine, Nederpelt)</a></p>
<p>let's come up with another one! (…see also Zena Ariola…)</p>
<p><a href="https://omega.googlecode.com/svn/wiki/LambdaGraph.svg" target="_blank"><img src="https://omega.googlecode.com/svn/wiki/LambdaGraph.svg" alt="Lambda Graph" style="max-width:100%;"></a></p>
</div>
<div class='slide markdown-body'><h2>
<a name="binary-search-tree" class="anchor" href="#binary-search-tree"></a>(Binary) search tree</h2>
<p>We start with a lambda term
<a href="https://github-camo.global.ssl.fastly.net/e0e700be099745e30bfdd218969ce2aa9f8c1390/687474703a2f2f6c617465782e636f6465636f67732e636f6d2f7376672e6c617465783f285c6c616d62646120782e787829285c6c616d62646120782e787829" target="_blank"><img src="https://github-camo.global.ssl.fastly.net/e0e700be099745e30bfdd218969ce2aa9f8c1390/687474703a2f2f6c617465782e636f6465636f67732e636f6d2f7376672e6c617465783f285c6c616d62646120782e787829285c6c616d62646120782e787829" border="0" style="max-width:100%;"></a></p>
<p>Respecting scope we build a search tree and retrofit it with references</p>
<p><a href="https://rawgithub.com/ggreif/seminar-opetope/master/y-comb.svg" target="_blank"><img src="https://rawgithub.com/ggreif/seminar-opetope/master/y-comb.svg" alt="Y combinator" style="max-width:100%;"></a></p>
<p>Kind for shapes</p>
<div class="highlight highlight-haskell"><pre><span class="nf">kind</span> <span class="kt">Sh</span> <span class="ow">=</span> <span class="kt">Ap</span> <span class="kt">Sh</span> <span class="kt">Sh</span> <span class="o">|</span> <span class="kt">Lm</span> <span class="kt">Sh</span> <span class="o">|</span> <span class="kt">Rf</span> <span class="kt">Ref</span>
<span class="nf">kind</span> <span class="kt">Ref</span> <span class="ow">=</span> <span class="kt">Up</span> <span class="kt">Ref</span> <span class="o">|</span> <span class="kt">Stop</span> <span class="o">|</span> <span class="kt">Left</span> <span class="kt">Ref</span> <span class="o">|</span> <span class="kt">Right</span> <span class="kt">Ref</span> <span class="o">|</span> <span class="kt">Down</span> <span class="kt">Ref</span>
</pre></div>
</div>
<div class='slide markdown-body'><h1>
<a name="abstraction--binders" class="anchor" href="#abstraction--binders"></a>Abstraction / Binders</h1>
<p>Key insight: Trees admit naturals</p>
<p><a href="https://rawgithub.com/ggreif/seminar-opetope/master/glue-downstream.svg" target="_blank"><img src="https://rawgithub.com/ggreif/seminar-opetope/master/glue-downstream.svg" alt="Glue input" style="max-width:100%;"></a></p>
<p>But we need <em>deBruijn</em> + <em>extra sauce</em></p>
<p><a href="https://rawgithub.com/ggreif/seminar-opetope/master/docking-stations.svg" target="_blank"><img src="https://rawgithub.com/ggreif/seminar-opetope/master/docking-stations.svg" alt="Docking stations" style="max-width:100%;"></a></p>
</div>
<div class='slide markdown-body'><h1>
<a name="references-identification-gluing" class="anchor" href="#references-identification-gluing"></a>References: Identification, gluing</h1>
<p><a href="https://rawgithub.com/ggreif/seminar-opetope/master/references.svg" target="_blank"><img src="https://rawgithub.com/ggreif/seminar-opetope/master/references.svg" alt="References" style="max-width:100%;"></a></p>
<ul>
<li>gluing an input on a (constructor) application ⟶ pattern matching</li>
<li>… means: "application dot" here</li>
<li>gluing inputs <em>vanish</em> from application dot</li>
<li>n-ary application possible? semantics?</li>
</ul></div>
<div class='slide markdown-body'><h1>
<a name="beta-reduction" class="anchor" href="#beta-reduction"></a>Beta-reduction</h1>
<p>When a selected external branch is <em>saturated</em> by application,
it completely dissolves, and the addressed binding station
gets glued to the argument.</p>
<p>Depending on the intended reduction strategy the <em>use</em> references
may be expanded (<em>unsharing</em>).</p>
</div>
<div class='slide markdown-body'><h1>
<a name="internal-hom" class="anchor" href="#internal-hom"></a>Internal Hom</h1>
<p><code>(→)</code> is binary type constructor</p>
<ul>
<li>profunctor (contra-/covariant)</li>
<li>Klein bottle (orientation-reversing)</li>
</ul></div>
<div class='slide markdown-body'><h1>
<a name="strata-in-%CE%A9mega" class="anchor" href="#strata-in-%CE%A9mega"></a>Strata in Ωmega</h1>
<p><a href="https://github-camo.global.ssl.fastly.net/8859cbfaee499e2c63877040ffd9b86250d18c96/687474703a2f2f6f6d6567612e676f6f676c65636f64652e636f6d2f73766e2f77696b692f4b696e642d6869657261726368792e737667" target="_blank"><img src="https://github-camo.global.ssl.fastly.net/8859cbfaee499e2c63877040ffd9b86250d18c96/687474703a2f2f6f6d6567612e676f6f676c65636f64652e636f6d2f73766e2f77696b692f4b696e642d6869657261726368792e737667" alt="Type strata" style="max-width:100%;"></a></p>
</div>
<div class='slide markdown-body'><h2>
<a name="singleton-types-in-haskell" class="anchor" href="#singleton-types-in-haskell"></a>Singleton Types in Haskell</h2>
<p>Kind promotion</p>
<p><a href="https://rawgithub.com/ggreif/seminar-opetope/master/haskell-nats.svg" target="_blank"><img src="https://rawgithub.com/ggreif/seminar-opetope/master/haskell-nats.svg" alt="Nat'" style="max-width:100%;"></a></p>
<div class="highlight highlight-haskell"><pre><span class="kr">data</span> <span class="cm">{- kind -}</span> <span class="kt">Nat</span> <span class="ow">=</span> <span class="kt">Z</span> <span class="o">|</span> <span class="kt">S</span> <span class="kt">Nat</span>
<span class="kr">data</span> <span class="kt">Nat'</span> <span class="ow">::</span> <span class="kt">Nat</span> <span class="ow">-></span> <span class="o">*</span> <span class="kr">where</span>
<span class="kt">Z'</span> <span class="ow">::</span> <span class="kt">Nat'</span> <span class="kt">Z</span>
<span class="kt">S'</span> <span class="ow">::</span> <span class="kt">Nat'</span> <span class="n">n</span> <span class="ow">-></span> <span class="kt">Nat'</span> <span class="p">(</span><span class="kt">S</span> <span class="n">n</span><span class="p">)</span>
</pre></div>
</div>
<div class='slide markdown-body'><h2>
<a name="singleton-types-in-%CE%A9mega" class="anchor" href="#singleton-types-in-%CE%A9mega"></a>Singleton Types in Ωmega</h2>
<p>Kind definitions possible (at any level)</p>
<p><a href="https://rawgithub.com/ggreif/seminar-opetope/master/omega-nats.svg" target="_blank"><img src="https://rawgithub.com/ggreif/seminar-opetope/master/omega-nats.svg" alt="Ωmega's Nat'" style="max-width:100%;"></a></p>
<div class="highlight highlight-haskell"><pre><span class="nf">kind</span> <span class="kt">Nat</span> <span class="ow">=</span> <span class="kt">Z</span> <span class="o">|</span> <span class="kt">S</span> <span class="kt">Nat</span>
<span class="kr">data</span> <span class="kt">Nat'</span> <span class="ow">::</span> <span class="kt">Nat</span> <span class="o">~></span> <span class="o">*</span> <span class="kr">where</span>
<span class="kt">Z'</span> <span class="ow">::</span> <span class="kt">Nat'</span> <span class="kt">Z</span>
<span class="kt">S'</span> <span class="ow">::</span> <span class="kt">Nat'</span> <span class="n">n</span> <span class="ow">-></span> <span class="kt">Nat'</span> <span class="p">(</span><span class="kt">S</span> <span class="n">n</span><span class="p">)</span>
</pre></div>
</div>
<div class='slide markdown-body'><h2>
<a name="level-polymorphism" class="anchor" href="#level-polymorphism"></a>Level Polymorphism</h2>
<div class="highlight highlight-haskell"><pre><span class="kr">data</span> <span class="kt">Nat</span> <span class="ow">::</span> <span class="n">level</span> <span class="n">k</span> <span class="o">.</span> <span class="o">*</span><span class="n">k</span> <span class="kr">where</span>
<span class="kt">Z</span> <span class="ow">::</span> <span class="kt">Nat</span>
<span class="kt">S</span> <span class="ow">::</span> <span class="kt">Nat</span> <span class="o">~></span> <span class="kt">Nat</span>
</pre></div>
<p><a href="https://rawgithub.com/ggreif/seminar-opetope/master/omega-levels.svg" target="_blank"><img src="https://rawgithub.com/ggreif/seminar-opetope/master/omega-levels.svg" alt="Ωmega's level polymorphism" style="max-width:100%;"></a></p>
</div>
<div class='slide markdown-body'><h2>
<a name="can-we-please-have-curry-howard-back" class="anchor" href="#can-we-please-have-curry-howard-back"></a>Can we please have Curry-Howard back?</h2>
<p>C-H lost as level-polymorphic type <code>Nat</code> above has no type parameter/index!</p>
<p>Idea: parametrize with the same thing, but from one level up...</p>
<p>Unfortunately this is not working out :-(</p>
<p>I tried:</p>
<p><a href="https://rawgithub.com/ggreif/seminar-opetope/master/singleton-levels.svg" target="_blank"><img src="https://rawgithub.com/ggreif/seminar-opetope/master/singleton-levels.svg" alt="A failure" style="max-width:100%;"></a></p>
<p>For a few levels (each differently named) <a href="https://code.google.com/p/omega/wiki/AutoLevelled#%CE%A9mega_example_for_%E2%80%B9%E2%80%B9Pat%E2%80%BA%E2%80%BA">it can be made</a>.</p>
</div>
<div class='slide markdown-body'><h2>
<a name="next-idea" class="anchor" href="#next-idea"></a>Next idea</h2>
<p>parametrize on the <strong>left</strong>. Make access to parameter <em>optional</em>.</p>
<p>these all mean the same thing:</p>
<div class="highlight highlight-haskell"><pre><span class="kt">S</span> <span class="kt">Z</span> <span class="ow">::</span> <span class="kt">Nat</span>
<span class="kt">S</span> <span class="kt">Z</span> <span class="ow">::</span> <span class="kt">S</span> <span class="kt">Z</span> <span class="err">°</span> <span class="kt">Nat</span>
<span class="kt">S</span> <span class="kt">Z</span> <span class="ow">::</span> <span class="p">(</span><span class="kt">S</span> <span class="kt">Z</span> <span class="ow">::</span> <span class="kt">Nat</span><span class="p">)</span> <span class="err">°</span> <span class="kt">Nat</span>
<span class="kt">S</span> <span class="kt">Z</span> <span class="ow">::</span> <span class="p">(</span><span class="kt">S</span> <span class="kt">Z</span> <span class="ow">::</span> <span class="kt">S</span> <span class="kt">Z</span> <span class="err">°</span> <span class="kt">Nat</span><span class="p">)</span> <span class="err">°</span> <span class="kt">Nat</span>
</pre></div>
<p>Ad infinitum, coinductively.</p>
</div>
<div class='slide markdown-body'><h2>
<a name="programming-in-the-sky" class="anchor" href="#programming-in-the-sky"></a><em>Programming in the Sky</em>
</h2>
<p>Program in the (co)limit. Write a very simple <code>data</code> definition</p>
<div class="highlight highlight-haskell"><pre><span class="kr">data</span> <span class="kt">Nat</span> <span class="ow">=</span> <span class="kt">Z</span> <span class="o">|</span> <span class="kt">S</span> <span class="kt">Nat</span>
</pre></div>
<p>… but have the refinement structure available when wanting to
state type-level propositions.</p>
</div>
<div class='slide markdown-body'><h1>
<a name="conclusion" class="anchor" href="#conclusion"></a>Conclusion</h1>
<ol>
<li>Opetopic calculus is rich and very interesting</li>
<li>It appears to be a solid basis for stratified type systems</li>
<li>Cartesian closure not completely understood yet</li>
</ol></div>
<div class='slide markdown-body'><h1>
<a name="questions" class="anchor" href="#questions"></a>Questions?</h1>
<p>Thanks for your attention!</p>
<p>Btw. I am looking for collaborators</p>
<ol>
<li>to make these ideas precise</li>
<li>kick-start an initial implementation.</li>
</ol>
</div>
</body>
</html>