intro

groupoid · Oct 29, 2023 · cb0841c · cb0841c
1 parent e88cf18
commit cb0841c
Show file tree

Hide file tree

Showing 2 changed files with 36 additions and 36 deletions.
diff --git a/intro/index.html b/intro/index.html
@@ -56,30 +56,30 @@
 дорівнюють між собою, отже
 простір шляхів утворює багатовимірну структуру
 інфініті-групоїда.
-</p><code>isProp <span class="h__symbol">(</span>A <span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span> <span class="h__symbol">:</span> <span class="h__keyword">U</span> <span class="h__symbol">:</span><span class="h__symbol">=</span> Π <span class="h__symbol">(</span>a b <span class="h__symbol">:</span> A<span class="h__symbol">)</span>,
-    <span class="h__keyword">Path</span> A a b
+</p><code><span class="h__keyword">def</span> isProp <span class="h__symbol">(</span>A <span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span> <span class="h__symbol">:</span> <span class="h__keyword">U</span>
+ <span class="h__symbol">:</span><span class="h__symbol">=</span> Π <span class="h__symbol">(</span>a b <span class="h__symbol">:</span> A<span class="h__symbol">)</span>, <span class="h__keyword">Path</span> A a b
 
-isSet <span class="h__symbol">(</span>A <span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span> <span class="h__symbol">:</span> <span class="h__keyword">U</span> <span class="h__symbol">:</span><span class="h__symbol">=</span> Π <span class="h__symbol">(</span>a b <span class="h__symbol">:</span> A<span class="h__symbol">)</span>
-    <span class="h__symbol">(</span>a0 b0 <span class="h__symbol">:</span> <span class="h__keyword">Path</span> A a b<span class="h__symbol">)</span>,
+<span class="h__keyword">def</span> isSet <span class="h__symbol">(</span>A <span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span> <span class="h__symbol">:</span> <span class="h__keyword">U</span>
+ <span class="h__symbol">:</span><span class="h__symbol">=</span> Π <span class="h__symbol">(</span>a b <span class="h__symbol">:</span> A<span class="h__symbol">)</span> <span class="h__symbol">(</span>a0 b0 <span class="h__symbol">:</span> <span class="h__keyword">Path</span> A a b<span class="h__symbol">)</span>,
     <span class="h__keyword">Path</span> <span class="h__symbol">(</span><span class="h__keyword">Path</span> A a b<span class="h__symbol">)</span> a0 b0
 
-isGroupoid <span class="h__symbol">(</span>A <span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span> <span class="h__symbol">:</span> <span class="h__keyword">U</span>
+<span class="h__keyword">def</span> isGroupoid <span class="h__symbol">(</span>A <span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span> <span class="h__symbol">:</span> <span class="h__keyword">U</span>
  <span class="h__symbol">:</span><span class="h__symbol">=</span> Π <span class="h__symbol">(</span>a b <span class="h__symbol">:</span> A<span class="h__symbol">)</span> <span class="h__symbol">(</span>x y <span class="h__symbol">:</span> <span class="h__keyword">Path</span> A a b<span class="h__symbol">)</span>
     <span class="h__symbol">(</span>i j <span class="h__symbol">:</span> <span class="h__keyword">Path</span> <span class="h__symbol">(</span><span class="h__keyword">Path</span> A a b<span class="h__symbol">)</span> x y<span class="h__symbol">)</span>,
     <span class="h__keyword">Path</span> <span class="h__symbol">(</span><span class="h__keyword">Path</span> <span class="h__symbol">(</span><span class="h__keyword">Path</span> A a b<span class="h__symbol">)</span> x y<span class="h__symbol">)</span> i j</code><br><p>Групоїдна інтерпретація теорії типів ставить питання про існування мови,
-в якій можна довести механічно всі всластивості категорного визначення групоїда.</p><code>CatGroupoid <span class="h__symbol">(</span>X <span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span> <span class="h__symbol">(</span>G <span class="h__symbol">:</span> isGroupoid X<span class="h__symbol">)</span>
-   <span class="h__symbol">:</span> isCatGroupoid <span class="h__symbol">(</span>PathCat X<span class="h__symbol">)</span>
-  <span class="h__symbol">:</span><span class="h__symbol">=</span> <span class="h__symbol">(</span> <span class="h__keyword">idp</span> X,
-       comp-<span class="h__keyword">Path</span> X,
-       G,
-       sym X,
-       comp-inv-<span class="h__keyword">Path</span>⁻¹ X,
-       comp-inv-<span class="h__keyword">Path</span> X,
-       comp-<span class="h__keyword">Path</span>-left X,
-       comp-<span class="h__keyword">Path</span>-right X,
-       comp-<span class="h__keyword">Path</span>-assoc X,
-       star
-     <span class="h__symbol">)</span></code><p>За цей час були перепробувані глобулярні та сімліціальні моделі, але
+в якій можна довести механічно всі всластивості категорного визначення групоїда.</p><code><span class="h__keyword">def</span> CatGroupoid <span class="h__symbol">(</span>X <span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span> <span class="h__symbol">(</span>G <span class="h__symbol">:</span> isGroupoid X<span class="h__symbol">)</span>
+  <span class="h__symbol">:</span> isCatGroupoid <span class="h__symbol">(</span>PathCat X<span class="h__symbol">)</span>
+ <span class="h__symbol">:</span><span class="h__symbol">=</span> <span class="h__symbol">(</span> <span class="h__keyword">idp</span> X,
+      comp-<span class="h__keyword">Path</span> X,
+      G,
+      sym X,
+      comp-inv-<span class="h__keyword">Path</span>⁻¹ X,
+      comp-inv-<span class="h__keyword">Path</span> X,
+      comp-<span class="h__keyword">Path</span>-left X,
+      comp-<span class="h__keyword">Path</span>-right X,
+      comp-<span class="h__keyword">Path</span>-assoc X,
+      ★
+    <span class="h__symbol">)</span></code><p>За цей час були перепробувані глобулярні та сімліціальні моделі, але
 аксіома унівалентності конструктивно валідується тільки в кубічних множинах,
 на рівні теорії типів це відбувається в Кан-операціях <mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.439ex;" xmlns="http://www.w3.org/2000/svg" width="6.305ex" height="1.83ex" role="img" focusable="false" viewBox="0 -615 2787 809" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1415-TEX-N-74" d="M27 422Q80 426 109 478T141 600V615H181V431H316V385H181V241Q182 116 182 100T189 68Q203 29 238 29Q282 29 292 100Q293 108 293 146V181H333V146V134Q333 57 291 17Q264 -10 221 -10Q187 -10 162 2T124 33T105 68T98 100Q97 107 97 248V385H18V422H27Z"></path><path id="MJX-1415-TEX-N-72" d="M36 46H50Q89 46 97 60V68Q97 77 97 91T98 122T98 161T98 203Q98 234 98 269T98 328L97 351Q94 370 83 376T38 385H20V408Q20 431 22 431L32 432Q42 433 60 434T96 436Q112 437 131 438T160 441T171 442H174V373Q213 441 271 441H277Q322 441 343 419T364 373Q364 352 351 337T313 322Q288 322 276 338T263 372Q263 381 265 388T270 400T273 405Q271 407 250 401Q234 393 226 386Q179 341 179 207V154Q179 141 179 127T179 101T180 81T180 66V61Q181 59 183 57T188 54T193 51T200 49T207 48T216 47T225 47T235 46T245 46H276V0H267Q249 3 140 3Q37 3 28 0H20V46H36Z"></path><path id="MJX-1415-TEX-N-61" d="M137 305T115 305T78 320T63 359Q63 394 97 421T218 448Q291 448 336 416T396 340Q401 326 401 309T402 194V124Q402 76 407 58T428 40Q443 40 448 56T453 109V145H493V106Q492 66 490 59Q481 29 455 12T400 -6T353 12T329 54V58L327 55Q325 52 322 49T314 40T302 29T287 17T269 6T247 -2T221 -8T190 -11Q130 -11 82 20T34 107Q34 128 41 147T68 188T116 225T194 253T304 268H318V290Q318 324 312 340Q290 411 215 411Q197 411 181 410T156 406T148 403Q170 388 170 359Q170 334 154 320ZM126 106Q126 75 150 51T209 26Q247 26 276 49T315 109Q317 116 318 175Q318 233 317 233Q309 233 296 232T251 223T193 203T147 166T126 106Z"></path><path id="MJX-1415-TEX-N-6E" d="M41 46H55Q94 46 102 60V68Q102 77 102 91T102 122T103 161T103 203Q103 234 103 269T102 328V351Q99 370 88 376T43 385H25V408Q25 431 27 431L37 432Q47 433 65 434T102 436Q119 437 138 438T167 441T178 442H181V402Q181 364 182 364T187 369T199 384T218 402T247 421T285 437Q305 442 336 442Q450 438 463 329Q464 322 464 190V104Q464 66 466 59T477 49Q498 46 526 46H542V0H534L510 1Q487 2 460 2T422 3Q319 3 310 0H302V46H318Q379 46 379 62Q380 64 380 200Q379 335 378 343Q372 371 358 385T334 402T308 404Q263 404 229 370Q202 343 195 315T187 232V168V108Q187 78 188 68T191 55T200 49Q221 46 249 46H265V0H257L234 1Q210 2 183 2T145 3Q42 3 33 0H25V46H41Z"></path><path id="MJX-1415-TEX-N-73" d="M295 316Q295 356 268 385T190 414Q154 414 128 401Q98 382 98 349Q97 344 98 336T114 312T157 287Q175 282 201 278T245 269T277 256Q294 248 310 236T342 195T359 133Q359 71 321 31T198 -10H190Q138 -10 94 26L86 19L77 10Q71 4 65 -1L54 -11H46H42Q39 -11 33 -5V74V132Q33 153 35 157T45 162H54Q66 162 70 158T75 146T82 119T101 77Q136 26 198 26Q295 26 295 104Q295 133 277 151Q257 175 194 187T111 210Q75 227 54 256T33 318Q33 357 50 384T93 424T143 442T187 447H198Q238 447 268 432L283 424L292 431Q302 440 314 448H322H326Q329 448 335 442V310L329 304H301Q295 310 295 316Z"></path><path id="MJX-1415-TEX-N-70" d="M36 -148H50Q89 -148 97 -134V-126Q97 -119 97 -107T97 -77T98 -38T98 6T98 55T98 106Q98 140 98 177T98 243T98 296T97 335T97 351Q94 370 83 376T38 385H20V408Q20 431 22 431L32 432Q42 433 61 434T98 436Q115 437 135 438T165 441T176 442H179V416L180 390L188 397Q247 441 326 441Q407 441 464 377T522 216Q522 115 457 52T310 -11Q242 -11 190 33L182 40V-45V-101Q182 -128 184 -134T195 -145Q216 -148 244 -148H260V-194H252L228 -193Q205 -192 178 -192T140 -191Q37 -191 28 -194H20V-148H36ZM424 218Q424 292 390 347T305 402Q234 402 182 337V98Q222 26 294 26Q345 26 384 80T424 218Z"></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="74" xlink:href="#MJX-1415-TEX-N-74"></use><use data-c="72" xlink:href="#MJX-1415-TEX-N-72" transform="translate(389,0)"></use><use data-c="61" xlink:href="#MJX-1415-TEX-N-61" transform="translate(781,0)"></use><use data-c="6E" xlink:href="#MJX-1415-TEX-N-6E" transform="translate(1281,0)"></use><use data-c="73" xlink:href="#MJX-1415-TEX-N-73" transform="translate(1837,0)"></use><use data-c="70" xlink:href="#MJX-1415-TEX-N-70" transform="translate(2231,0)"></use></g></g></g></g></svg></mjx-container> та <mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.439ex;" xmlns="http://www.w3.org/2000/svg" width="6.536ex" height="2.009ex" role="img" focusable="false" viewBox="0 -694 2889 888" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1416-TEX-N-68" d="M41 46H55Q94 46 102 60V68Q102 77 102 91T102 124T102 167T103 217T103 272T103 329Q103 366 103 407T103 482T102 542T102 586T102 603Q99 622 88 628T43 637H25V660Q25 683 27 683L37 684Q47 685 66 686T103 688Q120 689 140 690T170 693T181 694H184V367Q244 442 328 442Q451 442 463 329Q464 322 464 190V104Q464 66 466 59T477 49Q498 46 526 46H542V0H534L510 1Q487 2 460 2T422 3Q319 3 310 0H302V46H318Q379 46 379 62Q380 64 380 200Q379 335 378 343Q372 371 358 385T334 402T308 404Q263 404 229 370Q202 343 195 315T187 232V168V108Q187 78 188 68T191 55T200 49Q221 46 249 46H265V0H257L234 1Q210 2 183 2T145 3Q42 3 33 0H25V46H41Z"></path><path id="MJX-1416-TEX-N-63" d="M370 305T349 305T313 320T297 358Q297 381 312 396Q317 401 317 402T307 404Q281 408 258 408Q209 408 178 376Q131 329 131 219Q131 137 162 90Q203 29 272 29Q313 29 338 55T374 117Q376 125 379 127T395 129H409Q415 123 415 120Q415 116 411 104T395 71T366 33T318 2T249 -11Q163 -11 99 53T34 214Q34 318 99 383T250 448T370 421T404 357Q404 334 387 320Z"></path><path id="MJX-1416-TEX-N-6F" d="M28 214Q28 309 93 378T250 448Q340 448 405 380T471 215Q471 120 407 55T250 -10Q153 -10 91 57T28 214ZM250 30Q372 30 372 193V225V250Q372 272 371 288T364 326T348 362T317 390T268 410Q263 411 252 411Q222 411 195 399Q152 377 139 338T126 246V226Q126 130 145 91Q177 30 250 30Z"></path><path id="MJX-1416-TEX-N-6D" d="M41 46H55Q94 46 102 60V68Q102 77 102 91T102 122T103 161T103 203Q103 234 103 269T102 328V351Q99 370 88 376T43 385H25V408Q25 431 27 431L37 432Q47 433 65 434T102 436Q119 437 138 438T167 441T178 442H181V402Q181 364 182 364T187 369T199 384T218 402T247 421T285 437Q305 442 336 442Q351 442 364 440T387 434T406 426T421 417T432 406T441 395T448 384T452 374T455 366L457 361L460 365Q463 369 466 373T475 384T488 397T503 410T523 422T546 432T572 439T603 442Q729 442 740 329Q741 322 741 190V104Q741 66 743 59T754 49Q775 46 803 46H819V0H811L788 1Q764 2 737 2T699 3Q596 3 587 0H579V46H595Q656 46 656 62Q657 64 657 200Q656 335 655 343Q649 371 635 385T611 402T585 404Q540 404 506 370Q479 343 472 315T464 232V168V108Q464 78 465 68T468 55T477 49Q498 46 526 46H542V0H534L510 1Q487 2 460 2T422 3Q319 3 310 0H302V46H318Q379 46 379 62Q380 64 380 200Q379 335 378 343Q372 371 358 385T334 402T308 404Q263 404 229 370Q202 343 195 315T187 232V168V108Q187 78 188 68T191 55T200 49Q221 46 249 46H265V0H257L234 1Q210 2 183 2T145 3Q42 3 33 0H25V46H41Z"></path><path id="MJX-1416-TEX-N-70" d="M36 -148H50Q89 -148 97 -134V-126Q97 -119 97 -107T97 -77T98 -38T98 6T98 55T98 106Q98 140 98 177T98 243T98 296T97 335T97 351Q94 370 83 376T38 385H20V408Q20 431 22 431L32 432Q42 433 61 434T98 436Q115 437 135 438T165 441T176 442H179V416L180 390L188 397Q247 441 326 441Q407 441 464 377T522 216Q522 115 457 52T310 -11Q242 -11 190 33L182 40V-45V-101Q182 -128 184 -134T195 -145Q216 -148 244 -148H260V-194H252L228 -193Q205 -192 178 -192T140 -191Q37 -191 28 -194H20V-148H36ZM424 218Q424 292 390 347T305 402Q234 402 182 337V98Q222 26 294 26Q345 26 384 80T424 218Z"></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="68" xlink:href="#MJX-1416-TEX-N-68"></use><use data-c="63" xlink:href="#MJX-1416-TEX-N-63" transform="translate(556,0)"></use><use data-c="6F" xlink:href="#MJX-1416-TEX-N-6F" transform="translate(1000,0)"></use><use data-c="6D" xlink:href="#MJX-1416-TEX-N-6D" transform="translate(1500,0)"></use><use data-c="70" xlink:href="#MJX-1416-TEX-N-70" transform="translate(2333,0)"></use></g></g></g></g></svg></mjx-container>.
 </p><br><center>&dot;</center><p>[1]. Pelayo, Warren. Homotopy type theory and Voevodsky's univalent foundations. 2012.

diff --git a/intro/index.pug b/intro/index.pug
@@ -92,14 +92,14 @@ block content
                     інфініті-групоїда.
 
                 +code.
-                    isProp (A : U) : U := Π (a b : A),
-                        Path A a b
+                    def isProp (A : U) : U
+                     := Π (a b : A), Path A a b
 
-                    isSet (A : U) : U := Π (a b : A)
-                        (a0 b0 : Path A a b),
+                    def isSet (A : U) : U
+                     := Π (a b : A) (a0 b0 : Path A a b),
                         Path (Path A a b) a0 b0
 
-                    isGroupoid (A : U) : U
+                    def isGroupoid (A : U) : U
                      := Π (a b : A) (x y : Path A a b)
                         (i j : Path (Path A a b) x y),
                         Path (Path (Path A a b) x y) i j
@@ -108,19 +108,19 @@ block content
                     Групоїдна інтерпретація теорії типів ставить питання про існування мови,
                     в якій можна довести механічно всі всластивості категорного визначення групоїда.
                 +code.
-                    CatGroupoid (X : U) (G : isGroupoid X)
-                       : isCatGroupoid (PathCat X)
-                      := ( idp X,
-                           comp-Path X,
-                           G,
-                           sym X,
-                           comp-inv-Path⁻¹ X,
-                           comp-inv-Path X,
-                           comp-Path-left X,
-                           comp-Path-right X,
-                           comp-Path-assoc X,
-                           star
-                         )
+                    def CatGroupoid (X : U) (G : isGroupoid X)
+                      : isCatGroupoid (PathCat X)
+                     := ( idp X,
+                          comp-Path X,
+                          G,
+                          sym X,
+                          comp-inv-Path⁻¹ X,
+                          comp-inv-Path X,
+                          comp-Path-left X,
+                          comp-Path-right X,
+                          comp-Path-assoc X,
+                          ★
+                        )
                 +tex.
                     За цей час були перепробувані глобулярні та сімліціальні моделі, але
                     аксіома унівалентності конструктивно валідується тільки в кубічних множинах,