Merge branch 'main' of github.com:groupoid/anders

groupoid · Sep 26, 2023 · 6982e9e · 6982e9e
2 parents bb2f93c + e515672
commit 6982e9e
Show file tree

Hide file tree

Showing 49 changed files with 1,118 additions and 1,204 deletions.
diff --git a/footer.pug b/footer.pug
@@ -2,4 +2,4 @@
 footer.footer
     a(href='https://5ht.co/license/')
        img.footer__logo(src='https://longchenpa.guru/seal.png',width=50)
-    span.footer__copy 2021&mdash;2022 &copy; <a href="//groupoid.space/" style="color:Lavender;">Groupoïd Infinity</a>
+    span.footer__copy 2021&mdash;2023 &copy; <a href="//groupoid.space/" style="color:Lavender;">Groupoïd Infinity</a>
diff --git a/foundations/mltt/either/index.html b/foundations/mltt/either/index.html
@@ -8,4 +8,4 @@
 </style></head><body class="content"></body></html><html><head><meta property="og:title" content="EITHER"><meta property="og:description" content="Either"><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>
 <a href='https://anders.groupoid.space/lib/'>LIB</a>
 <a href='#'>EITHER</a></nav><article class="main list"><section><h1>EITHER</h1><aside><time>Published: 4 NOV 2017</time></aside><p><b>either</b> is a representation for sum types or disjunction.
-</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;2022 &copy; <a href="//groupoid.space/" style="color:Lavender;">Groupoïd Infinity</a></span></footer>
+</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>
diff --git a/foundations/mltt/id/index.html b/foundations/mltt/id/index.html
@@ -7,4 +7,4 @@
 use[data-c]{stroke-width:3px}
 </style></head><body class="content"></body></html><html><head><meta property="og:title" content="ID"><meta property="og:description" content="Equality types"><meta property="og:url" content="https://anders.groupoid.space/foundations/mltt/id/"></head></html><title>ID</title><nav><a href='https://anders.groupoid.space/'>ANDERS</a>
 <a href='https://anders.groupoid.space/lib/'>LIB</a>
-<a href='#'>ID</a></nav><article class="main list"><section><h1>ID</h1><aside><time>Published: 4 NOV 2021</time></aside><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;2022 &copy; <a href="//groupoid.space/" style="color:Lavender;">Groupoïd Infinity</a></span></footer>
+<a href='#'>ID</a></nav><article class="main list"><section><h1>ID</h1><aside><time>Published: 4 NOV 2021</time></aside><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>
diff --git a/foundations/mltt/inductive/index.html b/foundations/mltt/inductive/index.html
diff --git a/foundations/mltt/inductive/index.pug b/foundations/mltt/inductive/index.pug
@@ -20,7 +20,7 @@ block content
             aside
                 time Published: 27 JAN 2022
             p.
-                These types form the inductive basis of MLTT foundations
+                These types form the inductive basis of MLTT-80 foundations
                 and are built-in into type checker.
 
             h1 EMPTY

diff --git a/foundations/mltt/io/index.html b/foundations/mltt/io/index.html
@@ -15,4 +15,4 @@
 (main: IO.replicateM 100
        (IO.>>= IO.data () IO.getLine IO.putLine))
 
-</code></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;2022 &copy; <a href="//groupoid.space/" style="color:Lavender;">Groupoïd Infinity</a></span></footer>
+</code></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>
diff --git a/foundations/mltt/ioi/index.html b/foundations/mltt/ioi/index.html
@@ -26,4 +26,4 @@
                     (IOI.getLine r (Maybe IOI.data)
                                 (Maybe.Just IOI.data))))
 
-</code></section><div class="om"></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&mdash;2022 &copy; <a href="//groupoid.space/" style="color:Lavender;">Groupoïd Infinity</a></span></footer>
+</code></section><div class="om"></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&mdash;2023 &copy; <a href="//groupoid.space/" style="color:Lavender;">Groupoïd Infinity</a></span></footer>
diff --git a/foundations/mltt/list/index.html b/foundations/mltt/list/index.html
diff --git a/foundations/mltt/list/index.pug b/foundations/mltt/list/index.pug
@@ -19,16 +19,19 @@ block content
             h1 LIST
             aside
                 time Published: 4 NOV 2017
-            p.
-                The data type of <b>list</b> over a given set A can
-                be represented as the initial algebra (&mu;&nbsp;L<sub>A</sub>,&nbsp;in)
-                of the functor L<sub>A</sub>(X) = 1 + (A &times; X).
-                Denote &mu; L<sub>A</sub> = List(A). The constructor
-                functions nil: 1 &rightarrow; List(A) and cons: A
-                &times; List(A) &rightarrow; List(A) are defined
-                by nil = in ◦ inl and cons = in ◦ inr, so
-                in = <b>[nil,cons]</b>.
-            p.
+            +tex.
+                The data type of $list$ over a given set $A$ can
+                be represented as the initial algebra $(\mu\ L_A, in)$
+                of the functor $L_A(X) = 1 + (A \times X)$.
+                Denote $\mu L_A = List(A)$. The constructor
+                functions
+                $nil: 1 \rightarrow List(A)$ and
+                $cons: A \times List(A) \rightarrow List(A)$
+                are defined by
+                $nil = in \cdot inl$ and
+                $cons = in \cdot inr$, so
+                $in = [nil,cons]$.
+            +tex.
                 In type theory $List$ type could be expressed as
                 $$
                    List(A) := W_{(x:1+A)},\ rec_{1+A}(A,U,0,λa.𝟏,x).
@@ -38,17 +41,17 @@ block content
                 def List (A: U) := W (x : Maybe A), List-ctor A x
 
             h2 Constructors
-            p.
-                You can create zero list with <b>nil</b> and append an element
-                to the head of the list with <b>cons</b>.
+            +tex.
+                You can create zero list with $nil$ and append an element
+                to the head of the list with $cons$.
             code.
                 def nil (A: U) : List A
                 def cons (A: U) (x : A) (xs: List A) : List A
 
             h2 Induction Principle
-            p.
-               Induction principle allows you to prove general predicate on List (C n)
-               from predicates on constructors (C nil) and (C cons).
+            +tex.
+               Induction principle allows you to prove general predicate on $List (C\ n)$
+               from predicates on constructors $(C\ nil)$ and $(C\ cons)$.
             code.
                 def List-ind (A: U) (C: List A -> U)
                     (z: C (nil A)) (s: Π (x: A) (xs: List A), C xs -> C (cons A x xs))

diff --git a/foundations/mltt/maybe/index.html b/foundations/mltt/maybe/index.html
@@ -7,6 +7,6 @@
 use[data-c]{stroke-width:3px}
 </style></head><body class="content"></body></html><html><head><meta property="og:title" content="MAYBE"><meta property="og:description" content="Maybe"><meta property="og:url" content="https://anders.groupoid.space/foundations/mltt/maybe/"></head></html><title>MAYBE</title><nav><a href='https://anders.groupoid.space/'>ANDERS</a>
 <a href='https://anders.groupoid.space/lib/'>LIB</a>
-<a href='#'>MAYBE</a></nav><article class="main list"><section><h1>MAYBE</h1><aside><time>Published: 4 NOV 2017</time></aside><p>Maybe has representing functor M<sub>A</sub>(X) = 1 + A.
+<a href='#'>MAYBE</a></nav><article class="main list"><section><h1>MAYBE</h1><aside><time>Published: 4 NOV 2017</time></aside><p>Maybe has representing functor <mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.566ex;" xmlns="http://www.w3.org/2000/svg" width="15.881ex" height="2.262ex" role="img" focusable="false" viewBox="0 -750 7019.3 1000" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-837-TEX-I-1D440" d="M289 629Q289 635 232 637Q208 637 201 638T194 648Q194 649 196 659Q197 662 198 666T199 671T201 676T203 679T207 681T212 683T220 683T232 684Q238 684 262 684T307 683Q386 683 398 683T414 678Q415 674 451 396L487 117L510 154Q534 190 574 254T662 394Q837 673 839 675Q840 676 842 678T846 681L852 683H948Q965 683 988 683T1017 684Q1051 684 1051 673Q1051 668 1048 656T1045 643Q1041 637 1008 637Q968 636 957 634T939 623Q936 618 867 340T797 59Q797 55 798 54T805 50T822 48T855 46H886Q892 37 892 35Q892 19 885 5Q880 0 869 0Q864 0 828 1T736 2Q675 2 644 2T609 1Q592 1 592 11Q592 13 594 25Q598 41 602 43T625 46Q652 46 685 49Q699 52 704 61Q706 65 742 207T813 490T848 631L654 322Q458 10 453 5Q451 4 449 3Q444 0 433 0Q418 0 415 7Q413 11 374 317L335 624L267 354Q200 88 200 79Q206 46 272 46H282Q288 41 289 37T286 19Q282 3 278 1Q274 0 267 0Q265 0 255 0T221 1T157 2Q127 2 95 1T58 0Q43 0 39 2T35 11Q35 13 38 25T43 40Q45 46 65 46Q135 46 154 86Q158 92 223 354T289 629Z"></path><path id="MJX-837-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><path id="MJX-837-TEX-N-28" d="M94 250Q94 319 104 381T127 488T164 576T202 643T244 695T277 729T302 750H315H319Q333 750 333 741Q333 738 316 720T275 667T226 581T184 443T167 250T184 58T225 -81T274 -167T316 -220T333 -241Q333 -250 318 -250H315H302L274 -226Q180 -141 137 -14T94 250Z"></path><path id="MJX-837-TEX-I-1D44B" d="M42 0H40Q26 0 26 11Q26 15 29 27Q33 41 36 43T55 46Q141 49 190 98Q200 108 306 224T411 342Q302 620 297 625Q288 636 234 637H206Q200 643 200 645T202 664Q206 677 212 683H226Q260 681 347 681Q380 681 408 681T453 682T473 682Q490 682 490 671Q490 670 488 658Q484 643 481 640T465 637Q434 634 411 620L488 426L541 485Q646 598 646 610Q646 628 622 635Q617 635 609 637Q594 637 594 648Q594 650 596 664Q600 677 606 683H618Q619 683 643 683T697 681T738 680Q828 680 837 683H845Q852 676 852 672Q850 647 840 637H824Q790 636 763 628T722 611T698 593L687 584Q687 585 592 480L505 384Q505 383 536 304T601 142T638 56Q648 47 699 46Q734 46 734 37Q734 35 732 23Q728 7 725 4T711 1Q708 1 678 1T589 2Q528 2 496 2T461 1Q444 1 444 10Q444 11 446 25Q448 35 450 39T455 44T464 46T480 47T506 54Q523 62 523 64Q522 64 476 181L429 299Q241 95 236 84Q232 76 232 72Q232 53 261 47Q262 47 267 47T273 46Q276 46 277 46T280 45T283 42T284 35Q284 26 282 19Q279 6 276 4T261 1Q258 1 243 1T201 2T142 2Q64 2 42 0Z"></path><path id="MJX-837-TEX-N-29" d="M60 749L64 750Q69 750 74 750H86L114 726Q208 641 251 514T294 250Q294 182 284 119T261 12T224 -76T186 -143T145 -194T113 -227T90 -246Q87 -249 86 -250H74Q66 -250 63 -250T58 -247T55 -238Q56 -237 66 -225Q221 -64 221 250T66 725Q56 737 55 738Q55 746 60 749Z"></path><path id="MJX-837-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><path id="MJX-837-TEX-N-31" d="M213 578L200 573Q186 568 160 563T102 556H83V602H102Q149 604 189 617T245 641T273 663Q275 666 285 666Q294 666 302 660V361L303 61Q310 54 315 52T339 48T401 46H427V0H416Q395 3 257 3Q121 3 100 0H88V46H114Q136 46 152 46T177 47T193 50T201 52T207 57T213 61V578Z"></path><path id="MJX-837-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="msub"><g data-mml-node="mi"><use data-c="1D440" xlink:href="#MJX-837-TEX-I-1D440"></use></g><g data-mml-node="mi" transform="translate(1003,-152.7) scale(0.707)"><use data-c="1D434" xlink:href="#MJX-837-TEX-I-1D434"></use></g></g><g data-mml-node="mo" transform="translate(1583.3,0)"><use data-c="28" xlink:href="#MJX-837-TEX-N-28"></use></g><g data-mml-node="mi" transform="translate(1972.3,0)"><use data-c="1D44B" xlink:href="#MJX-837-TEX-I-1D44B"></use></g><g data-mml-node="mo" transform="translate(2824.3,0)"><use data-c="29" xlink:href="#MJX-837-TEX-N-29"></use></g><g data-mml-node="mo" transform="translate(3491.1,0)"><use data-c="3D" xlink:href="#MJX-837-TEX-N-3D"></use></g><g data-mml-node="mn" transform="translate(4546.9,0)"><use data-c="31" xlink:href="#MJX-837-TEX-N-31"></use></g><g data-mml-node="mo" transform="translate(5269.1,0)"><use data-c="2B" xlink:href="#MJX-837-TEX-N-2B"></use></g><g data-mml-node="mi" transform="translate(6269.3,0)"><use data-c="1D434" xlink:href="#MJX-837-TEX-I-1D434"></use></g></g></g></svg></mjx-container>.
 It is used for wrapping values with optional nothing constructor.
-</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;2022 &copy; <a href="//groupoid.space/" style="color:Lavender;">Groupoïd Infinity</a></span></footer>
+</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>
diff --git a/foundations/mltt/maybe/index.pug b/foundations/mltt/maybe/index.pug
@@ -19,8 +19,8 @@ block content
             h1 MAYBE
             aside
                 time Published: 4 NOV 2017
-            p.
-                Maybe has representing functor M<sub>A</sub>(X) = 1 + A.
+            +tex.
+                Maybe has representing functor $M_A(X) = 1 + A$.
                 It is used for wrapping values with optional nothing constructor.
 
             h2 Constructors