ABCFHL in univalent foundations

groupoid · Oct 29, 2023 · 4364122 · 4364122
1 parent c6d981c
commit 4364122
Show file tree

Hide file tree

Showing 21 changed files with 97 additions and 27 deletions.
diff --git a/foundations/mltt/either/index.html b/foundations/mltt/either/index.html
@@ -5,7 +5,7 @@
 .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="EITHER"><meta property="og:description" content="Either type (disjunction)"><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>
+</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>
 <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: 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.
 </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/either/index.pug b/foundations/mltt/either/index.pug
@@ -3,7 +3,7 @@ include ../../../header
 html
     head
         meta(property='og:title'       content='EITHER')
-        meta(property='og:description' content='Either type (disjunction)')
+        meta(property='og:description' content='Either type (disjunction, union)')
         meta(property='og:url'         content='https://anders.groupoid.space/foundations/mltt/either/')
 
 block title

diff --git a/foundations/mltt/id/index.html b/foundations/mltt/id/index.html
@@ -5,7 +5,7 @@
 .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="ID"><meta property="og:description" content="Identity Spaces"><meta property="og:url" content="https://anders.groupoid.space/foundations/mltt/id/"></head></html><title>ID</title><nav><a href='../../../index.html'>ANDERS</a>
+</style></head><body class="content"></body></html><html><head><meta property="og:title" content="ID"><meta property="og:description" content="Identity Space"><meta property="og:url" content="https://anders.groupoid.space/foundations/mltt/id/"></head></html><title>ID</title><nav><a href='../../../index.html'>ANDERS</a>
 <a href='../../../lib/index.html'>LIB</a>
 <a href='#'>ID</a></nav><article class="main list"><section><h1>IDENTITY SPACES</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-2-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-2-TEX-N-3D"></use></g></g></g></svg></mjx-container>-type is an inductive family that contains evidence
 of equality of two elements from that family. 

diff --git a/foundations/mltt/id/index.pug b/foundations/mltt/id/index.pug
@@ -3,7 +3,7 @@ include ../../../header
 html
     head
         meta(property='og:title'       content='ID')
-        meta(property='og:description' content='Identity Spaces')
+        meta(property='og:description' content='Identity Space')
         meta(property='og:url'         content='https://anders.groupoid.space/foundations/mltt/id/')
 
 block title

diff --git a/foundations/mltt/inductive/index.html b/foundations/mltt/inductive/index.html
@@ -5,7 +5,7 @@
 .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="INDUCTIVE"><meta property="og:description" content="Inductive MLTT Foundations"><meta property="og:url" content="https://anders.groupoid.space/foundations/mltt/inductive/"></head></html><title>INDUCTIVE</title><nav><a href='../../../index.html'>ANDERS</a>
+</style></head><body class="content"></body></html><html><head><meta property="og:title" content="INDUCTIVE"><meta property="og:description" content="Inductive Space"><meta property="og:url" content="https://anders.groupoid.space/foundations/mltt/inductive/"></head></html><title>INDUCTIVE</title><nav><a href='../../../index.html'>ANDERS</a>
 <a href='../../../lib/index.html'>LIB</a>
 <a href='#'>INDUCTIVE</a></nav><article class="main list"><section><h1>INDUCTIVE SPACES</h1><aside><time>Published: 7 OCT 2017</time></aside><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.439ex;" xmlns="http://www.w3.org/2000/svg" width="1.93ex" height="1.919ex" role="img" focusable="false" viewBox="0 -654 853 848" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-46-TEX-N-1D7CE" d="M266 654H280H282Q500 654 524 418Q529 370 529 320Q529 125 456 52Q397 -10 287 -10Q110 -10 63 154Q45 212 45 316Q45 504 113 585Q140 618 185 636T266 654ZM374 548Q347 604 286 604Q247 604 218 575Q197 552 193 511T188 311Q188 159 196 116Q202 87 225 64T287 41Q339 41 367 87Q379 107 382 152T386 329Q386 518 374 548Z"></path><path id="MJX-46-TEX-N-2C" d="M78 35T78 60T94 103T137 121Q165 121 187 96T210 8Q210 -27 201 -60T180 -117T154 -158T130 -185T117 -194Q113 -194 104 -185T95 -172Q95 -168 106 -156T131 -126T157 -76T173 -3V9L172 8Q170 7 167 6T161 3T152 1T140 0Q113 0 96 17Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mn"><use data-c="1D7CE" xlink:href="#MJX-46-TEX-N-1D7CE"></use></g><g data-mml-node="mo" transform="translate(575,0)"><use data-c="2C" xlink:href="#MJX-46-TEX-N-2C"></use></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="1.93ex" height="1.921ex" role="img" focusable="false" viewBox="0 -655 853 849" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-47-TEX-N-1D7CF" d="M481 0L294 3Q136 3 109 0H96V62H227V304Q227 546 225 546Q169 529 97 529H80V591H97Q231 591 308 647L319 655H333Q355 655 359 644Q361 640 361 351V62H494V0H481Z"></path><path id="MJX-47-TEX-N-2C" d="M78 35T78 60T94 103T137 121Q165 121 187 96T210 8Q210 -27 201 -60T180 -117T154 -158T130 -185T117 -194Q113 -194 104 -185T95 -172Q95 -168 106 -156T131 -126T157 -76T173 -3V9L172 8Q170 7 167 6T161 3T152 1T140 0Q113 0 96 17Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mn"><use data-c="1D7CF" xlink:href="#MJX-47-TEX-N-1D7CF"></use></g><g data-mml-node="mo" transform="translate(575,0)"><use data-c="2C" xlink:href="#MJX-47-TEX-N-2C"></use></g></g></g></svg></mjx-container> <mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: 0;" xmlns="http://www.w3.org/2000/svg" width="1.301ex" height="1.48ex" role="img" focusable="false" viewBox="0 -654 575 654" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-48-TEX-N-1D7D0" d="M175 580Q175 578 185 572T205 551T215 510Q215 467 191 449T137 430Q107 430 83 448T58 511Q58 558 91 592T168 640T259 654Q328 654 383 637Q451 610 484 563T517 459Q517 401 482 360T368 262Q340 243 265 184L210 140H274Q416 140 429 145Q439 148 447 186T455 237H517V233Q516 230 501 119Q489 9 486 4V0H57V25Q57 51 58 54Q60 57 109 106T215 214T288 291Q364 377 364 458Q364 515 328 553T231 592Q214 592 201 589T181 584T175 580Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mn"><use data-c="1D7D0" xlink:href="#MJX-48-TEX-N-1D7D0"></use></g></g></g></svg></mjx-container> form the inductive base for well-founded
 spaces <mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.05ex;" xmlns="http://www.w3.org/2000/svg" width="2.326ex" height="1.595ex" role="img" focusable="false" viewBox="0 -683 1028 705" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-49-TEX-N-57" d="M792 683Q810 680 914 680Q991 680 1003 683H1009V637H996Q931 633 915 598Q912 591 863 438T766 135T716 -17Q711 -22 694 -22Q676 -22 673 -15Q671 -13 593 231L514 477L435 234Q416 174 391 92T358 -6T341 -22H331Q314 -21 310 -15Q309 -14 208 302T104 622Q98 632 87 633Q73 637 35 637H18V683H27Q69 681 154 681Q164 681 181 681T216 681T249 682T276 683H287H298V637H285Q213 637 213 620Q213 616 289 381L364 144L427 339Q490 535 492 546Q487 560 482 578T475 602T468 618T461 628T449 633T433 636T408 637H380V683H388Q397 680 508 680Q629 680 650 683H660V637H647Q576 637 576 619L727 146Q869 580 869 600Q869 605 863 612T839 627T794 637H783V683H792Z"></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="57" xlink:href="#MJX-49-TEX-N-57"></use></g></g></g></g></svg></mjx-container> of MLTT-80 that allow to manipulate F-algebras.

diff --git a/foundations/mltt/inductive/index.pug b/foundations/mltt/inductive/index.pug
@@ -3,7 +3,7 @@ include ../../../header
 html
     head
         meta(property='og:title'       content='INDUCTIVE')
-        meta(property='og:description' content='Inductive MLTT Foundations')
+        meta(property='og:description' content='Inductive Space')
         meta(property='og:url'         content='https://anders.groupoid.space/foundations/mltt/inductive/')
 
 block title

diff --git a/foundations/mltt/io/index.html b/foundations/mltt/io/index.html
@@ -11,7 +11,10 @@
 foldNat  Zero    f x <span class="h__symbol">=</span> x
 foldNat <span class="h__symbol">(</span>Succ m<span class="h__symbol">)</span> f x <span class="h__symbol">=</span> f <span class="h__symbol">(</span>foldNat m f x<span class="h__symbol">)</span>
 
-data IO r <span class="h__symbol">=</span> PutStrLn String <span class="h__symbol">(</span>IO r<span class="h__symbol">)</span> | GetLine <span class="h__symbol">(</span>String -> IO r<span class="h__symbol">)</span> | Return r
+data IO r
+   <span class="h__symbol">=</span> PutStrLn String <span class="h__symbol">(</span>IO r<span class="h__symbol">)</span>
+   | GetLine <span class="h__symbol">(</span>String -> IO r<span class="h__symbol">)</span>
+   | Return r
 
 putStrLn <span class="h__symbol">:</span> String -> IO <span class="h__keyword">U</span>
 putStrLn str <span class="h__symbol">=</span> PutStrLn str <span class="h__symbol">(</span>Return Unit<span class="h__symbol">)</span>
@@ -27,6 +30,7 @@
 
 replicateM <span class="h__symbol">:</span> Nat -> IO <span class="h__keyword">U</span> -> IO <span class="h__keyword">U</span>
 replicateM n io <span class="h__symbol">=</span> foldNat n <span class="h__symbol">(</span>io >><span class="h__symbol">)</span> <span class="h__symbol">(</span>return Unit<span class="h__symbol">)</span>
-io <span class="h__symbol">:</span> IO <span class="h__keyword">U</span>
+
+recursion <span class="h__symbol">:</span> IO <span class="h__keyword">U</span> -- over Nat
    <span class="h__symbol">=</span> replicateM 5 <span class="h__symbol">(</span>getLine >><span class="h__symbol">=</span> putStrLn<span class="h__symbol">)</span>
 </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/io/index.pug b/foundations/mltt/io/index.pug
@@ -20,7 +20,10 @@ block content
                 foldNat  Zero    f x = x
                 foldNat (Succ m) f x = f (foldNat m f x)
 
-                data IO r = PutStrLn String (IO r) | GetLine (String -> IO r) | Return r
+                data IO r
+                   = PutStrLn String (IO r)
+                   | GetLine (String -> IO r)
+                   | Return r
 
                 putStrLn : String -> IO U
                 putStrLn str = PutStrLn str (Return Unit)
@@ -36,7 +39,8 @@ block content
 
                 replicateM : Nat -> IO U -> IO U
                 replicateM n io = foldNat n (io >>) (return Unit)
-                io : IO U
+
+                recursion : IO U -- over Nat
                    = replicateM 5 (getLine >>= putStrLn)
 
 include ../../../footer
diff --git a/foundations/mltt/ioi/index.html b/foundations/mltt/ioi/index.html
@@ -12,10 +12,30 @@
    | GetLine <span class="h__symbol">(</span>String -> s<span class="h__symbol">)</span>
    | Return r
 
+maybe <span class="h__symbol">:</span> <span class="h__symbol">(</span>a -> b<span class="h__symbol">)</span> -> b -> Maybe a -> b
+Just <span class="h__symbol">:</span> a -> Maybe a
+
 data IOI r
    <span class="h__symbol">=</span> forall s . MkIO s <span class="h__symbol">(</span>s -> IOF r s<span class="h__symbol">)</span>
 
-io <span class="h__symbol">:</span> IOI
-   <span class="h__symbol">=</span> MkIO Nothing <span class="h__symbol">(</span>maybe <span class="h__symbol">(</span>\str -> PutStrLn str Nothing<span class="h__symbol">)</span>
-                         <span class="h__symbol">(</span>GetLine Just<span class="h__symbol">))</span>
-</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>
+corecursion <span class="h__symbol">:</span> IOI <span class="h__symbol">()</span>
+   <span class="h__symbol">=</span> MkIO
+     Nothing
+     <span class="h__symbol">(</span>maybe <span class="h__symbol">(</span>\ s -> PutStrLn s Nothing<span class="h__symbol">)</span>
+            <span class="h__symbol">(</span>GetLine Just<span class="h__symbol">))</span></code><br><p>In pure functions:</p><code>   \ <span class="h__symbol">(</span>r <span class="h__symbol">:</span> *1<span class="h__symbol">)</span>
+-> #IOI/MkIO r
+   <span class="h__symbol">(</span>#Maybe/@ #IOI/data<span class="h__symbol">)</span>
+   <span class="h__symbol">(</span>#Maybe/Nothing #IOI/data<span class="h__symbol">)</span>
+   <span class="h__symbol">(</span> \ <span class="h__symbol">(</span>m <span class="h__symbol">:</span> #Maybe/@ #IOI/data<span class="h__symbol">)</span>
+    -> #Maybe/maybe #IOI/data m
+       <span class="h__symbol">(</span>#IOI/F r <span class="h__symbol">(</span>#Maybe/@ #IOI/data<span class="h__symbol">))</span>
+       <span class="h__symbol">(</span> \ <span class="h__symbol">(</span>str <span class="h__symbol">:</span> #IOI/data<span class="h__symbol">)</span>
+        -> #IOI/putLine r
+           <span class="h__symbol">(</span>#Maybe/@ #IOI/data<span class="h__symbol">)</span> str
+           <span class="h__symbol">(</span>#Maybe/Nothing #IOI/data<span class="h__symbol">)</span>
+       <span class="h__symbol">)</span>
+       <span class="h__symbol">(</span> #IOI/getLine r
+         <span class="h__symbol">(</span>#Maybe/@ #IOI/data<span class="h__symbol">)</span>
+         <span class="h__symbol">(</span>#Maybe/Just #IOI/data<span class="h__symbol">)</span>
+       <span class="h__symbol">)</span>
+  <span class="h__symbol">)</span></code><br></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.pug b/foundations/mltt/ioi/index.pug
@@ -20,11 +20,38 @@ block content
                    | GetLine (String -> s)
                    | Return r
 
+                maybe : (a -> b) -> b -> Maybe a -> b
+                Just : a -> Maybe a
+
                 data IOI r
                    = forall s . MkIO s (s -> IOF r s)
 
-                io : IOI
-                   = MkIO Nothing (maybe (\str -> PutStrLn str Nothing)
-                                         (GetLine Just))
+                corecursion : IOI ()
+                   = MkIO
+                     Nothing
+                     (maybe (\ s -> PutStrLn s Nothing)
+                            (GetLine Just))
+            br.
+            p.
+                In pure functions:
+            +code.
+                   \ (r : *1)
+                -> #IOI/MkIO r
+                   (#Maybe/@ #IOI/data)
+                   (#Maybe/Nothing #IOI/data)
+                   ( \ (m : #Maybe/@ #IOI/data)
+                    -> #Maybe/maybe #IOI/data m
+                       (#IOI/F r (#Maybe/@ #IOI/data))
+                       ( \ (str : #IOI/data)
+                        -> #IOI/putLine r
+                           (#Maybe/@ #IOI/data) str
+                           (#Maybe/Nothing #IOI/data)
+                       )
+                       ( #IOI/getLine r
+                         (#Maybe/@ #IOI/data)
+                         (#Maybe/Just #IOI/data)
+                       )
+                  )
+            br.
 
 include ../../../footer