Skip to content

Commit eae2c0c

Browse files
5HT5HT
committed
fmt
1 parent 7c3b55e commit eae2c0c

File tree

38 files changed

+38
-38
lines changed

38 files changed

+38
-38
lines changed

‎footer.pug‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,4 +2,4 @@
22
footer.footer
33
a(href='https://5ht.co/license/')
44
img.footer__logo(src='https://longchenpa.guru/seal.png',width=50)
5-
span.footer__copy 2021&mdash;2023 &copy; <a href="//groupoid.space/" style="color:Lavender;">Groupoïd Infinity</a>
5+
span.footer__copy 2021&mdash;2025 &copy; <a href="//groupoid.space/" style="color:Lavender;">Groupoïd Infinity</a>

‎foundations/mltt/either/index.html‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,4 +8,4 @@
88
</style></head><body class="content"></body></html><html><head><meta property="og:title" content="EITHER"><meta property="og:description" content="Either type (disjunction, union)"><meta property="og:url" content="https://anders.groupoid.space/foundations/mltt/either/"></head></html><title>EITHER</title><nav><a href='https://anders.groupoid.space/'>ANDERS</a>
99
<a href='https://anders.groupoid.space/lib/'>LIB</a>
1010
<a href='#'>EITHER</a></nav><article class="main list"><section><h1>EITHER</h1><aside><time>Published: 16 OCT 2017</time></aside><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.186ex;" xmlns="http://www.w3.org/2000/svg" width="1.76ex" height="1.505ex" role="img" focusable="false" viewBox="0 -583 778 665" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1-TEX-N-2B" d="M56 237T56 250T70 270H369V420L370 570Q380 583 389 583Q402 583 409 568V270H707Q722 262 722 250T707 230H409V-68Q401 -82 391 -82H389H387Q375 -82 369 -68V230H70Q56 237 56 250Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mo"><use data-c="2B" xlink:href="#MJX-1-TEX-N-2B"></use></g></g></g></svg></mjx-container>-type is a representation disjunction.
11-
</p><h2>Constructors</h2><h2>Eliminators</h2><h2>Induction Principle</h2></section></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&mdash;2023 &copy; <a href="//groupoid.space/" style="color:Lavender;">Groupoïd Infinity</a></span></footer>
11+
</p><h2>Constructors</h2><h2>Eliminators</h2><h2>Induction Principle</h2></section></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&mdash;2025 &copy; <a href="//groupoid.space/" style="color:Lavender;">Groupoïd Infinity</a></span></footer>

‎foundations/mltt/id/index.html‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,4 +52,4 @@
5252
system (<mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.186ex;" xmlns="http://www.w3.org/2000/svg" width="1.76ex" height="1.505ex" role="img" focusable="false" viewBox="0 -583 778 665" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-41-TEX-N-3D" d="M56 347Q56 360 70 367H707Q722 359 722 347Q722 336 708 328L390 327H72Q56 332 56 347ZM56 153Q56 168 72 173H708Q722 163 722 153Q722 140 707 133H70Q56 140 56 153Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mo"><use data-c="3D" xlink:href="#MJX-41-TEX-N-3D"></use></g></g></g></svg></mjx-container>), which respects UIP.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.025ex;" xmlns="http://www.w3.org/2000/svg" width="15.24ex" height="1.609ex" role="img" focusable="false" viewBox="0 -700 6736 711" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-42-TEX-B-1D403" d="M39 624V686H270H310H408Q500 686 545 680T638 649Q768 584 805 438Q817 388 817 338Q817 171 702 75Q628 17 515 2Q504 1 270 0H39V62H147V624H39ZM655 337Q655 370 655 390T650 442T639 494T616 540T580 580T526 607T451 623Q443 624 368 624H298V62H377H387H407Q445 62 472 65T540 83T606 129Q629 156 640 195T653 262T655 337Z"></path><path id="MJX-42-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-42-TEX-B-1D41F" d="M308 0Q290 3 172 3Q58 3 49 0H40V62H109V382H42V444H109V503L110 562L112 572Q127 625 178 658T316 699Q318 699 330 699T348 700Q381 698 404 687T436 658T449 629T452 606Q452 576 432 557T383 537Q355 537 335 555T314 605Q314 635 328 649H325Q311 649 293 644T253 618T227 560Q226 555 226 498V444H340V382H232V62H318V0H308Z"></path><path id="MJX-42-TEX-B-1D422" d="M72 610Q72 649 98 672T159 695Q193 693 217 670T241 610Q241 572 217 549T157 525Q120 525 96 548T72 610ZM46 442L136 446L226 450H232V62H294V0H286Q271 3 171 3Q67 3 49 0H40V62H109V209Q109 358 108 362Q103 380 55 380H43V442H46Z"></path><path id="MJX-42-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-42-TEX-B-1D42D" d="M272 49Q320 49 320 136V145V177H382V143Q382 106 380 99Q374 62 349 36T285 -2L272 -5H247Q173 -5 134 27Q109 46 102 74T94 160Q94 171 94 199T95 245V382H21V433H25Q58 433 90 456Q121 479 140 523T162 621V635H224V444H363V382H224V239V207V149Q224 98 228 81T249 55Q261 49 272 49Z"></path><path id="MJX-42-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-42-TEX-B-A0" d=""></path><path id="MJX-42-TEX-B-1D7D1" d="M80 503Q80 565 133 610T274 655Q366 655 421 623T491 538Q493 528 493 510Q493 446 453 407T361 348L376 344Q452 324 489 281T526 184Q526 152 514 121T474 58T392 8T265 -11Q175 -11 111 34T48 152Q50 187 72 209T132 232Q171 232 193 208T216 147Q216 136 214 126T207 108T197 94T187 84T178 77T170 72L168 71Q168 70 179 65T215 54T266 48H270Q331 48 350 105Q358 128 358 185Q358 239 348 268T309 313Q292 321 242 322Q205 322 198 324T191 341V348Q191 366 196 369T232 375Q239 375 247 376T260 377T268 378Q284 383 297 393T326 436T341 517Q341 536 339 547T331 573T308 593T266 600Q248 600 241 599Q214 593 183 576Q234 556 234 503Q234 462 210 444T157 426Q126 426 103 446T80 503Z"></path><path id="MJX-42-TEX-B-2E" d="M74 85Q74 121 99 146T156 171Q200 171 222 143T245 85Q245 56 224 29T160 1Q118 1 96 27T74 85Z"></path><path id="MJX-42-TEX-B-1D7D7" d="M178 59Q206 48 238 48Q311 48 345 102Q370 138 375 259V278Q374 278 369 271T350 252T322 232Q297 220 258 220Q172 220 110 275T48 438V446Q54 561 146 618Q199 654 278 654Q321 654 329 653Q526 621 526 330Q526 252 507 190T457 92T388 31T312 -2T240 -11Q165 -11 121 25T77 120Q77 159 99 176T147 193T194 177T217 122Q217 113 216 106T211 92T205 82T198 73T191 67T184 62T178 59ZM374 446V465Q374 523 364 552T315 598Q309 600 293 601Q227 601 210 562Q199 539 199 433Q199 343 204 319T235 279Q250 272 274 271H282Q293 271 303 274T327 288T353 323T371 385Q374 403 374 446Z"></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="1D403" xlink:href="#MJX-42-TEX-B-1D403"></use><use data-c="1D41E" xlink:href="#MJX-42-TEX-B-1D41E" transform="translate(882,0)"></use><use data-c="1D41F" xlink:href="#MJX-42-TEX-B-1D41F" transform="translate(1409,0)"></use><use data-c="1D422" xlink:href="#MJX-42-TEX-B-1D422" transform="translate(1760,0)"></use><use data-c="1D427" xlink:href="#MJX-42-TEX-B-1D427" transform="translate(2079,0)"></use><use data-c="1D422" xlink:href="#MJX-42-TEX-B-1D422" transform="translate(2718,0)"></use><use data-c="1D42D" xlink:href="#MJX-42-TEX-B-1D42D" transform="translate(3037,0)"></use><use data-c="1D422" xlink:href="#MJX-42-TEX-B-1D422" transform="translate(3484,0)"></use><use data-c="1D428" xlink:href="#MJX-42-TEX-B-1D428" transform="translate(3803,0)"></use><use data-c="1D427" xlink:href="#MJX-42-TEX-B-1D427" transform="translate(4378,0)"></use></g><g data-mml-node="mtext" transform="translate(5017,0)"><use data-c="A0" xlink:href="#MJX-42-TEX-B-A0"></use></g><g data-mml-node="mn" transform="translate(5267,0)"><use data-c="1D7D1" xlink:href="#MJX-42-TEX-B-1D7D1"></use><use data-c="2E" xlink:href="#MJX-42-TEX-B-2E" transform="translate(575,0)"></use><use data-c="1D7D7" xlink:href="#MJX-42-TEX-B-1D7D7" transform="translate(894,0)"></use></g></g></g></g></svg></mjx-container> (Homotopy Identity System). An identity system
5353
over type <mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: 0;" xmlns="http://www.w3.org/2000/svg" width="1.697ex" height="1.62ex" role="img" focusable="false" viewBox="0 -716 750 716" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-43-TEX-I-1D434" d="M208 74Q208 50 254 46Q272 46 272 35Q272 34 270 22Q267 8 264 4T251 0Q249 0 239 0T205 1T141 2Q70 2 50 0H42Q35 7 35 11Q37 38 48 46H62Q132 49 164 96Q170 102 345 401T523 704Q530 716 547 716H555H572Q578 707 578 706L606 383Q634 60 636 57Q641 46 701 46Q726 46 726 36Q726 34 723 22Q720 7 718 4T704 0Q701 0 690 0T651 1T578 2Q484 2 455 0H443Q437 6 437 9T439 27Q443 40 445 43L449 46H469Q523 49 533 63L521 213H283L249 155Q208 86 208 74ZM516 260Q516 271 504 416T490 562L463 519Q447 492 400 412L310 260L413 259Q516 259 516 260Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mi"><use data-c="1D434" xlink:href="#MJX-43-TEX-I-1D434"></use></g></g></g></svg></mjx-container> and universe of homotopy types <mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.357ex;" xmlns="http://www.w3.org/2000/svg" width="2.285ex" height="1.902ex" role="img" focusable="false" viewBox="0 -683 1010 840.8" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-44-TEX-I-1D448" d="M107 637Q73 637 71 641Q70 643 70 649Q70 673 81 682Q83 683 98 683Q139 681 234 681Q268 681 297 681T342 682T362 682Q378 682 378 672Q378 670 376 658Q371 641 366 638H364Q362 638 359 638T352 638T343 637T334 637Q295 636 284 634T266 623Q265 621 238 518T184 302T154 169Q152 155 152 140Q152 86 183 55T269 24Q336 24 403 69T501 205L552 406Q599 598 599 606Q599 633 535 637Q511 637 511 648Q511 650 513 660Q517 676 519 679T529 683Q532 683 561 682T645 680Q696 680 723 681T752 682Q767 682 767 672Q767 650 759 642Q756 637 737 637Q666 633 648 597Q646 592 598 404Q557 235 548 205Q515 105 433 42T263 -22Q171 -22 116 34T60 167V183Q60 201 115 421Q164 622 164 628Q164 635 107 637Z"></path><path id="MJX-44-TEX-I-1D456" d="M184 600Q184 624 203 642T247 661Q265 661 277 649T290 619Q290 596 270 577T226 557Q211 557 198 567T184 600ZM21 287Q21 295 30 318T54 369T98 420T158 442Q197 442 223 419T250 357Q250 340 236 301T196 196T154 83Q149 61 149 51Q149 26 166 26Q175 26 185 29T208 43T235 78T260 137Q263 149 265 151T282 153Q302 153 302 143Q302 135 293 112T268 61T223 11T161 -11Q129 -11 102 10T74 74Q74 91 79 106T122 220Q160 321 166 341T173 380Q173 404 156 404H154Q124 404 99 371T61 287Q60 286 59 284T58 281T56 279T53 278T49 278T41 278H27Q21 284 21 287Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="msub"><g data-mml-node="mi"><use data-c="1D448" xlink:href="#MJX-44-TEX-I-1D448"></use></g><g data-mml-node="mi" transform="translate(716,-150) scale(0.707)"><use data-c="1D456" xlink:href="#MJX-44-TEX-I-1D456"></use></g></g></g></g></svg></mjx-container> is called homotopy identity
5454
system (<mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: 0.081ex;" xmlns="http://www.w3.org/2000/svg" width="1.76ex" height="0.968ex" role="img" focusable="false" viewBox="0 -464 778 428" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-45-TEX-N-2261" d="M56 444Q56 457 70 464H707Q722 456 722 444Q722 430 706 424H72Q56 429 56 444ZM56 237T56 250T70 270H707Q722 262 722 250T707 230H70Q56 237 56 250ZM56 56Q56 71 72 76H706Q722 70 722 56Q722 44 707 36H70Q56 43 56 56Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mo"><use data-c="2261" xlink:href="#MJX-45-TEX-N-2261"></use></g></g></g></svg></mjx-container>), which models discrete infinity groupoid.
55-
</p></section></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&mdash;2023 &copy; <a href="//groupoid.space/" style="color:Lavender;">Groupoïd Infinity</a></span></footer>
55+
</p></section></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&mdash;2025 &copy; <a href="//groupoid.space/" style="color:Lavender;">Groupoïd Infinity</a></span></footer>

0 commit comments

Comments
 (0)