-
Notifications
You must be signed in to change notification settings - Fork 13
/
index.htm
77 lines (76 loc) · 26.2 KB
/
index.htm
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
<!DOCTYPE html><html><head><meta charset="utf-8"><meta http-equiv="x-ua-compatible" content="ie=edge"><meta property="fb:app_id" content="118554188236439"><meta name="viewport" content="width=device-width, initial-scale=1"><meta name="author" content="Maxim Sokhatsky"><meta name="twitter:site" content="@5HT"><meta name="twitter:creator" content="@5HT"><meta property="og:type" content="website"><meta property="og:image" content="https://avatars.githubusercontent.com/u/17128096?s=400&u=66a63d4cdd9625b2b4b37d724cc00fe6401e5bd8&v=4"><meta name="msapplication-TileColor" content="#ffffff"><meta name="msapplication-TileImage" content="https://anders.groupoid.space/images/ms-icon-144x144.png"><meta name="theme-color" content="#ffffff"><link rel="stylesheet" href="https://groupoid.github.io/axiom.dev/main.css"><link rel="apple-touch-icon" sizes="57x57" href="https://anders.groupoid.space/images/apple-icon-57x57.png"><link rel="apple-touch-icon" sizes="60x60" href="https://anders.groupoid.space/images/apple-icon-60x60.png"><link rel="apple-touch-icon" sizes="72x72" href="https://anders.groupoid.space/images/apple-icon-72x72.png"><link rel="apple-touch-icon" sizes="76x76" href="https://anders.groupoid.space/images/apple-icon-76x76.png"><link rel="apple-touch-icon" sizes="114x114" href="https://anders.groupoid.space/images/apple-icon-114x114.png"><link rel="apple-touch-icon" sizes="120x120" href="https://anders.groupoid.space/images/apple-icon-120x120.png"><link rel="apple-touch-icon" sizes="144x144" href="https://anders.groupoid.space/images/apple-icon-144x144.png"><link rel="apple-touch-icon" sizes="152x152" href="https://anders.groupoid.space/images/apple-icon-152x152.png"><link rel="apple-touch-icon" sizes="180x180" href="https://anders.groupoid.space/images//apple-icon-180x180.png"><link rel="icon" type="image/png" sizes="192x192" href="https://anders.groupoid.space/images/android-icon-192x192.png"><link rel="icon" type="image/png" sizes="32x32" href="https://anders.groupoid.space/images/favicon-32x32.png"><link rel="icon" type="image/png" sizes="96x96" href="https://anders.groupoid.space/images/favicon-96x96.png"><link rel="icon" type="image/png" sizes="16x16" href="https://anders.groupoid.space/images/favicon-16x16.png"><link rel="manifest" href="https://anders.groupoid.space/images/manifest.json"><style>svg a{fill:blue;stroke:blue}
[data-mml-node="merror"]>g{fill:red;stroke:red}
[data-mml-node="merror"]>rect[data-background]{fill:yellow;stroke:none}
[data-frame],[data-line]{stroke-width:70px;fill:none}
.mjx-dashed{stroke-dasharray:140}
.mjx-dotted{stroke-linecap:round;stroke-dasharray:0,140}
use[data-c]{stroke-width:3px}
</style></head><body class="content"></body></html><html><head><meta property="og:title" content="FORMAL/1"><meta property="og:description" content="Formal One"><meta property="og:url" content="https://groupoid.github.io/formal.one/"></head></html><title>AXIO/1</title><header class="header"><div class="header__titles"><h1 class="header__title">AXIO/1</h1><h4 class="header__subtitle">Формальне середовище виконання, система вищих мов та базові бібліотеки для програмування, доведення теорем і формальної філософії</h4></div></header><article class="main"><div class="om"><section><h1>Анотація</h1></section><aside><a href="https://tonpa.guru">Максим Сохацький</a><time>9 SEP 2021</time></aside><p>Перша формальна система AXIO/1 визначає формальний підхід до математичної
верифікації та описує спробу автора у цій парадигмі побудувати
замкнену уніфіковану систему формальних мов для програмування,
математики та філософії. В процесі розробки моделі такої
системи автору довелося апробувати частини її імплементації
для головних SML-подібних формальних академічних мов, мови
Erlang та інших (загалом 7 мов). За 10 років автором було
проаналізовані синтаксис та семантика основних мов програмування
(більше 50 мов) з різних промислових та академічних доменів,
8 мов з яких були особисто реалізовані автором. В роботі описані
8 мов уніфікованої мовної системи (концептуальна модель)
та представлені 2 їх імплементації.</p><p>Головним чином, натхнення було почерпнуте з LISP-машин
минулого, APL-систем, перших систем доведення теорем таких
як AUTOMATH, віртуальних маших паралельної та узгодженої
обробки нескінченних процесів, таких як BEAM, та кубічних MLTT-пруверів.
</p><section><h1>СТРУКТУРА</h1></section><p>Суть роботи полягає в побудові унікальної замкненої си-
стеми яка складається з:
1) системного програмного забезпечення – модального середовища
виконання разом з інтерпретатором написаним на формальній мові;
2) бібліотека та архітектура прикладного програмування N2O.TECH для середовищ виконання;
3) прикладного програмного забезпечення — системи вищих формальних мов,
для яких надано моделі, імплементації;
4) базова бібліотека разом з математичними компонентами (програми на вищих мовах).
</p></div><h2>Середовище виконання</h2><div class="index"><div class="index__col"><h2>Ядро</h2><ul><li><a href="https://groupoid.space/runtime/cps/">Інтерпретатор</a></li><li><a href="https://groupoid.space/runtime/apl/">Тензори</a></li><li><a href="https://groupoid.space/runtime/intercore/">Планувальник</a></li><li><a href="https://anders.groupoid.space/foundations/modal/process/">Процеси</a></li></ul></div><div class="index__col"><h2>Бібліотека</h2><ul><li><a href="https://groupoid.space/runtime/effects/">Протоколи</a></li><li><a href="https://anders.groupoid.space/foundations/mltt/io/">IO</a></li><li><a href="https://anders.groupoid.space/foundations/mltt/ioi/">IOI</a></li></ul></div></div><h2>Вищі мови програмування</h2><div class="index"><div class="index__col"><h2>Ядро PTS/PTS/MLTT</h2><ul><li><a href="https://henk.groupoid.space">Чисте-ядро</a></li><li><a href="https://groupoid.space/misc/semantics/">Фібраційне-ядро</a></li></ul></div><div class="index__col"><h2>HTS/CCHM і Бібліотека</h2><ul><li><a href="https://anders.groupoid.space/">Гомотопічне ядро</a></li><li><a href="https://groupoid.space/misc/library/">Математичні компоненти</a></li><li><a href="https://groupoid.space/misc/course/">Курс по теорії типів</a></li><li><a href="https://anders.groupoid.space/mathematics/homotopy/hopf/">Розшарування хопфа</a></li></ul></div></div><div class="om"><section><h1>Середовище виконання</h1></section><p>Синтансичне дерево мови інтерпретатора містить модуль лінивих
відкладених обчислень (CPS), та розширення синтаксичного
дерева спеціальними командами пов’язаними з середовищем
виконання (управління процесами виконання).
Програми таких інтерпретаторів виконуються у певній пам’яті,
яка використовується як контекст виконання. Кожна така програма
виконується як атомарний поток інструкцій на одному ядрі фізичного процесора.
Ситема віртуальних процесів містить SMP/AMP планувальник, який
управлє CPS-програмами які виконують інтерпретатори на кожному з фізичних ядер процесора.</p><p>Мотивація для побудови інтерпретатору, який повністю розміщується
разом з программою в L1 кеші (який лімітований 64КБ-256КБ) базується
на успіху таких віртуальних машин як LuaJIT, V8, HotSpot,
а також векторних мов програмування типу К та J. Якби ми могли
побудувати дійсно швидкий інтерпретатор який би виконував програми цілком в L1 кеші, байткод та
стріми якого були би вирівняні по словам архітектури, а для векторних
обчислень застосовувалися би AVX інструкції, які, як відомо
перемагають по ціні-якості GPU обчислення, то такий інтерпретатор міг би,
навіть без спеціалізованої JIT компіляції, скласти конкуренцію
сучасним промисловим інтерпретаторам, таким як Erlang, Python, K, LuaJIT.
Для дослідження цієї гіпотези мною було побудовано експериментальний
інтерпретатор без байт-коду, але з вирівняним по словам архітерктури
стрімом команд, які є безпосередньою машинною презентацією конструкторів індуктивних типів (enum)
мови Rust.</p><p>Ключовим викликом тут стали лінійні типи мови Rust, які не
дозволяють звертатися до посилань, які вже були оброблені, а це
впливає на всю архітектуру тензорного преставлення змінних в
мові інтерпретатор CPS, яка наслідує певним чином мову К.</p><p>Середовище виконання мість базову бібліотеку формалізовану в PureScript,
а також серію експериментів <a href="https://n2o.dev">N2O.DEV</a>,
повні версіх яких доступні для мови Erlang, Elixir та Hamler.
</p><section><h1>Вищі мови програмування</h1></section><p>Тут йдеться про мови програмування придатні для доведення
теорем, та їх таксономію від найелементарніших (чистої системи
з одним типом Π) до найпотужніших гомотопічних систем. Одна
така гомотопічна система є кінцевим завданням цього розділу
— побудова моделі гомотопічного верифікатора. В процесі його
побудови в цьому розділі ми розглянемо під мікроскопом складові частини його нижчих мовних рівнів.
Застосуємо категорну семантику для мов програмування і будемо розглядати мови програмування як моноїдальні
мовні категорі, об’єкти яких є просторами усіх програм цих мов програмування,
а морфізми — правила верифікації та компіляції цих програм.
Мови розкладаються у спектральну (індексовану натуральними числами N → U)
послідовність мов, кожен елемент якої є мовою програмування,
яка не містить синтаксичне дерево вищої мови програмування.</p><p>Система вищих мов мість базові бібліотеки PURE для системи PTS
та HOMOTOPY для системи MLTT/CCHM/HTS. Для побудови вищих мов
використовувалися мови OCaml та Erlang.
</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.011ex;" xmlns="http://www.w3.org/2000/svg" width="7.891ex" height="1.59ex" role="img" focusable="false" viewBox="0 -698 3488 703" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1-TEX-B-1D400" d="M296 0Q278 3 164 3Q58 3 49 0H40V62H92Q144 62 144 64Q388 682 397 689Q403 698 434 698Q463 698 471 689Q475 686 538 530T663 218L724 64Q724 62 776 62H828V0H817Q796 3 658 3Q509 3 485 0H472V62H517Q561 62 561 63L517 175H262L240 120Q218 65 217 64Q217 62 261 62H306V0H296ZM390 237L492 238L440 365Q390 491 388 491Q287 239 287 237H390Z"></path><path id="MJX-1-TEX-B-1D425" d="M43 686L134 690Q225 694 226 694H232V62H301V0H292Q274 3 170 3Q67 3 49 0H40V62H109V332Q109 387 109 453T110 534Q110 593 108 605T94 620Q80 624 53 624H40V686H43Z"></path><path id="MJX-1-TEX-B-1D428" d="M287 -5Q228 -5 182 10T109 48T63 102T39 161T32 219Q32 272 50 314T94 382T154 423T214 446T265 452H279Q319 452 326 451Q428 439 485 376T542 221Q542 156 514 108T442 33Q384 -5 287 -5ZM399 230V250Q399 280 398 298T391 338T372 372T338 392T282 401Q241 401 212 380Q190 363 183 334T175 230Q175 202 175 189T177 153T183 118T195 91T215 68T245 56T287 50Q348 50 374 84Q388 101 393 132T399 230Z"></path><path id="MJX-1-TEX-B-1D427" d="M40 442Q217 450 218 450H224V407L225 365Q233 378 245 391T289 422T362 448Q374 450 398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path><path id="MJX-1-TEX-B-1D433" d="M48 262Q48 264 54 349T60 436V444H252Q289 444 336 444T394 445Q441 445 450 441T459 418Q459 406 458 404Q456 399 327 229T194 55H237Q260 56 268 56T297 58T325 65T348 77T370 98T384 128T395 170Q400 197 400 216Q400 217 431 217H462V211Q461 208 453 108T444 6V0H245Q46 0 43 2Q32 7 32 28V33Q32 41 40 52T84 112Q129 170 164 217L298 393H256Q189 392 165 380Q124 360 115 303Q110 280 110 256Q110 254 79 254H48V262Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D400" xlink:href="#MJX-1-TEX-B-1D400"></use><use data-c="1D425" xlink:href="#MJX-1-TEX-B-1D425" transform="translate(869,0)"></use><use data-c="1D428" xlink:href="#MJX-1-TEX-B-1D428" transform="translate(1188,0)"></use><use data-c="1D427" xlink:href="#MJX-1-TEX-B-1D427" transform="translate(1763,0)"></use><use data-c="1D433" xlink:href="#MJX-1-TEX-B-1D433" transform="translate(2402,0)"></use><use data-c="1D428" xlink:href="#MJX-1-TEX-B-1D428" transform="translate(2913,0)"></use></g></g></g></g></svg></mjx-container> — просто типізоване лямбда-числення Каррі.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.014ex;" xmlns="http://www.w3.org/2000/svg" width="6.048ex" height="1.584ex" role="img" focusable="false" viewBox="0 -694 2673 700" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-2-TEX-B-1D407" d="M400 0Q376 3 226 3Q75 3 51 0H39V62H147V624H39V686H51Q75 683 226 683Q376 683 400 686H412V624H304V388H595V624H487V686H499Q523 683 673 683Q824 683 848 686H860V624H752V62H860V0H848Q824 3 674 3Q523 3 499 0H487V62H595V326H304V62H412V0H400Z"></path><path id="MJX-2-TEX-B-1D41E" d="M32 225Q32 332 102 392T272 452H283Q382 452 436 401Q494 343 494 243Q494 226 486 222T440 217Q431 217 394 217T327 218H175V209Q175 177 179 154T196 107T236 69T306 50Q312 49 323 49Q376 49 410 85Q421 99 427 111T434 127T442 133T463 135H468Q494 135 494 117Q494 110 489 97T468 66T431 32T373 5T292 -6Q181 -6 107 55T32 225ZM383 276Q377 346 348 374T280 402Q253 402 230 390T195 357Q179 331 176 279V266H383V276Z"></path><path id="MJX-2-TEX-B-1D427" d="M40 442Q217 450 218 450H224V407L225 365Q233 378 245 391T289 422T362 448Q374 450 398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path><path id="MJX-2-TEX-B-1D424" d="M32 686L123 690Q214 694 215 694H221V255L377 382H346V444H355Q370 441 476 441Q544 441 556 444H562V382H476L347 277L515 62H587V0H579Q564 3 476 3Q370 3 352 0H343V62H358L373 63L260 206L237 189L216 172V62H285V0H277Q259 3 157 3Q46 3 37 0H29V62H98V332Q98 387 98 453T99 534Q99 593 97 605T83 620Q69 624 42 624H29V686H32Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D407" xlink:href="#MJX-2-TEX-B-1D407"></use><use data-c="1D41E" xlink:href="#MJX-2-TEX-B-1D41E" transform="translate(900,0)"></use><use data-c="1D427" xlink:href="#MJX-2-TEX-B-1D427" transform="translate(1427,0)"></use><use data-c="1D424" xlink:href="#MJX-2-TEX-B-1D424" transform="translate(2066,0)"></use></g></g></g></g></svg></mjx-container> — чиста система з всвесвітами Кокана.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.014ex;" xmlns="http://www.w3.org/2000/svg" width="4.043ex" height="1.566ex" role="img" focusable="false" viewBox="0 -686 1787 692" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-3-TEX-B-1D40F" d="M400 0Q376 3 226 3Q75 3 51 0H39V62H147V624H39V686H253Q435 686 470 685T536 678Q585 668 621 648T675 605T705 557T718 514T721 483T718 451T704 409T673 362T616 322T530 293Q500 288 399 287H304V62H412V0H400ZM553 475Q553 554 537 582T459 622Q451 623 373 624H298V343H372Q457 344 480 350Q527 362 540 390T553 475Z"></path><path id="MJX-3-TEX-B-1D41E" d="M32 225Q32 332 102 392T272 452H283Q382 452 436 401Q494 343 494 243Q494 226 486 222T440 217Q431 217 394 217T327 218H175V209Q175 177 179 154T196 107T236 69T306 50Q312 49 323 49Q376 49 410 85Q421 99 427 111T434 127T442 133T463 135H468Q494 135 494 117Q494 110 489 97T468 66T431 32T373 5T292 -6Q181 -6 107 55T32 225ZM383 276Q377 346 348 374T280 402Q253 402 230 390T195 357Q179 331 176 279V266H383V276Z"></path><path id="MJX-3-TEX-B-1D42B" d="M405 293T374 293T324 312T305 361Q305 378 312 394Q315 397 315 399Q305 399 294 394T266 375T238 329T222 249Q221 241 221 149V62H308V0H298Q280 3 161 3Q47 3 38 0H29V62H98V210V303Q98 353 96 363T83 376Q69 380 42 380H29V442H32L118 446Q204 450 205 450H210V414L211 378Q247 449 315 449H321Q384 449 413 422T442 360Q442 332 424 313Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D40F" xlink:href="#MJX-3-TEX-B-1D40F"></use><use data-c="1D41E" xlink:href="#MJX-3-TEX-B-1D41E" transform="translate(786,0)"></use><use data-c="1D42B" xlink:href="#MJX-3-TEX-B-1D42B" transform="translate(1313,0)"></use></g></g></g></g></svg></mjx-container> — система Поулін-Моурін.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.014ex;" xmlns="http://www.w3.org/2000/svg" width="8.149ex" height="1.593ex" role="img" focusable="false" viewBox="0 -698 3602 704" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-4-TEX-B-1D400" d="M296 0Q278 3 164 3Q58 3 49 0H40V62H92Q144 62 144 64Q388 682 397 689Q403 698 434 698Q463 698 471 689Q475 686 538 530T663 218L724 64Q724 62 776 62H828V0H817Q796 3 658 3Q509 3 485 0H472V62H517Q561 62 561 63L517 175H262L240 120Q218 65 217 64Q217 62 261 62H306V0H296ZM390 237L492 238L440 365Q390 491 388 491Q287 239 287 237H390Z"></path><path id="MJX-4-TEX-B-1D427" d="M40 442Q217 450 218 450H224V407L225 365Q233 378 245 391T289 422T362 448Q374 450 398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path><path id="MJX-4-TEX-B-1D41D" d="M351 686L442 690Q533 694 534 694H540V389Q540 327 540 253T539 163Q539 97 541 83T555 66Q569 62 596 62H609V31Q609 0 608 0Q588 0 510 -3T412 -6Q411 -6 411 16V38L401 31Q337 -6 265 -6Q159 -6 99 58T38 224Q38 265 51 303T92 375T165 429T272 449Q359 449 417 412V507V555Q417 597 415 607T402 620Q388 624 361 624H348V686H351ZM411 350Q362 399 291 399Q278 399 256 392T218 371Q195 351 189 320T182 238V221Q182 179 183 159T191 115T212 74Q241 46 288 46Q358 46 404 100L411 109V350Z"></path><path id="MJX-4-TEX-B-1D41E" d="M32 225Q32 332 102 392T272 452H283Q382 452 436 401Q494 343 494 243Q494 226 486 222T440 217Q431 217 394 217T327 218H175V209Q175 177 179 154T196 107T236 69T306 50Q312 49 323 49Q376 49 410 85Q421 99 427 111T434 127T442 133T463 135H468Q494 135 494 117Q494 110 489 97T468 66T431 32T373 5T292 -6Q181 -6 107 55T32 225ZM383 276Q377 346 348 374T280 402Q253 402 230 390T195 357Q179 331 176 279V266H383V276Z"></path><path id="MJX-4-TEX-B-1D42B" d="M405 293T374 293T324 312T305 361Q305 378 312 394Q315 397 315 399Q305 399 294 394T266 375T238 329T222 249Q221 241 221 149V62H308V0H298Q280 3 161 3Q47 3 38 0H29V62H98V210V303Q98 353 96 363T83 376Q69 380 42 380H29V442H32L118 446Q204 450 205 450H210V414L211 378Q247 449 315 449H321Q384 449 413 422T442 360Q442 332 424 313Z"></path><path id="MJX-4-TEX-B-1D42C" d="M38 315Q38 339 45 360T70 404T127 440T223 453Q273 453 320 436L338 445L357 453H366Q380 453 383 447T386 403V387V355Q386 331 383 326T365 321H355H349Q333 321 329 324T324 341Q317 406 224 406H216Q123 406 123 353Q123 334 143 321T188 304T244 294T285 286Q305 281 325 273T373 237T412 172Q414 162 414 142Q414 -6 230 -6Q154 -6 117 22L68 -6H58Q44 -6 41 0T38 42V73Q38 85 38 101T37 122Q37 144 42 148T68 153H75Q87 153 91 151T97 147T103 132Q131 46 220 46H230Q257 46 265 47Q330 58 330 108Q330 127 316 142Q300 156 284 162Q271 168 212 178T122 202Q38 243 38 315Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D400" xlink:href="#MJX-4-TEX-B-1D400"></use><use data-c="1D427" xlink:href="#MJX-4-TEX-B-1D427" transform="translate(869,0)"></use><use data-c="1D41D" xlink:href="#MJX-4-TEX-B-1D41D" transform="translate(1508,0)"></use><use data-c="1D41E" xlink:href="#MJX-4-TEX-B-1D41E" transform="translate(2147,0)"></use><use data-c="1D42B" xlink:href="#MJX-4-TEX-B-1D42B" transform="translate(2674,0)"></use><use data-c="1D42C" xlink:href="#MJX-4-TEX-B-1D42C" transform="translate(3148,0)"></use></g></g></g></g></svg></mjx-container> — гомотопічна система з двома рівностями.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.025ex;" xmlns="http://www.w3.org/2000/svg" width="4.102ex" height="1.577ex" role="img" focusable="false" viewBox="0 -686 1813 697" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-5-TEX-B-1D414" d="M570 686Q588 683 703 683T836 686H845V624H737V420Q737 390 737 345T738 284Q738 205 729 164T689 83Q614 -11 465 -11Q321 -11 240 51T148 207Q147 214 147 421V624H39V686H51Q75 683 226 683Q376 683 400 686H412V624H304V405V370V268Q304 181 311 146T346 87Q387 52 466 52Q642 52 667 195Q668 204 669 415V624H561V686H570Z"></path><path id="MJX-5-TEX-B-1D42B" d="M405 293T374 293T324 312T305 361Q305 378 312 394Q315 397 315 399Q305 399 294 394T266 375T238 329T222 249Q221 241 221 149V62H308V0H298Q280 3 161 3Q47 3 38 0H29V62H98V210V303Q98 353 96 363T83 376Q69 380 42 380H29V442H32L118 446Q204 450 205 450H210V414L211 378Q247 449 315 449H321Q384 449 413 422T442 360Q442 332 424 313Z"></path><path id="MJX-5-TEX-B-1D42C" d="M38 315Q38 339 45 360T70 404T127 440T223 453Q273 453 320 436L338 445L357 453H366Q380 453 383 447T386 403V387V355Q386 331 383 326T365 321H355H349Q333 321 329 324T324 341Q317 406 224 406H216Q123 406 123 353Q123 334 143 321T188 304T244 294T285 286Q305 281 325 273T373 237T412 172Q414 162 414 142Q414 -6 230 -6Q154 -6 117 22L68 -6H58Q44 -6 41 0T38 42V73Q38 85 38 101T37 122Q37 144 42 148T68 153H75Q87 153 91 151T97 147T103 132Q131 46 220 46H230Q257 46 265 47Q330 58 330 108Q330 127 316 142Q300 156 284 162Q271 168 212 178T122 202Q38 243 38 315Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D414" xlink:href="#MJX-5-TEX-B-1D414"></use><use data-c="1D42B" xlink:href="#MJX-5-TEX-B-1D42B" transform="translate(885,0)"></use><use data-c="1D42C" xlink:href="#MJX-5-TEX-B-1D42C" transform="translate(1359,0)"></use></g></g></g></g></svg></mjx-container> — еквіваріантна супергомотопічна система типів.
</p></div><div class="index"><center><table cellspacing=5><tr><td width=5><img src="https://n2o.space/img/pdf.jpg" width=35></td><td width=400>
<a href="https://groupoid.github.io/formal.one/monography.pdf">
<h3>МОНОГРАФІЯ.PDF</h3>
</a></td></tr></table></center></div></article><footer class="footer"><a href="https://5ht.co/license/"><img class="footer__logo" src="https://longchenpa.guru/seal.png" width="50"></a><span class="footer__copy">2021—2022 © <a href="//groupoid.space/" style="color:Lavender;">Groupoïd Infinity</a></span><script src="https://groupoid.space/highlight.js"></script><script src="https://groupoid.space/bundle.js"></script></footer>