links, index

Author: 5HT

index.html

@@ -18,7 +18,7 @@
 </p><section><div class="macro"><div class="macro__col"><h3 id="categories"><b>ANALYSIS</b></h3><ol><li><a href='https://anders.groupoid.space/mathematics/analysis/topology/'>TOPOLOGY</a></li><li><a href='https://anders.groupoid.space/mathematics/analysis/set/'>SET</a></li><li><a href='https://anders.groupoid.space/mathematics/analysis/rational/'>ℚ</a>,
 <a href='https://anders.groupoid.space/mathematics/analysis/real/'>ℝ</a></li><li><a href='https://anders.groupoid.space/mathematics/analysis/complex/'>ℂ</a>,
 <a href='https://anders.groupoid.space/mathematics/analysis/quatro/'>ℍ</a>,
-<a href='https://anders.groupoid.space/mathematics/analysis/octo/'>𝕆</a></li></ol></div><div class="macro__col"><h3 id="algebra"><b>ALGEBRA</b></h3><ol><li><a href="https://anders.groupoid.space/mathematics/algebra/group/">GROUP</a></li><li><a href="https://anders.groupoid.space/mathematics/algebra/algebra/">ALGEBRA</a></li><li><a href="https://anders.groupoid.space/mathematics/algebra/homology/">HOMOLOGY</a></li></ol></div><div class="macro__col"><h3 id="geometry"><b>GEOMETRY</b></h3><ol><li><a href="https://anders.groupoid.space/mathematics/geometry/etale/">ETALE</a></li><li><a href="https://anders.groupoid.space/mathematics/geometry/bundle/">BUNDLE</a></li><li><a href="https://anders.groupoid.space/mathematics/geometry/manifold/">MANIFOLD</a></li><li><a href="https://anders.groupoid.space/mathematics/geometry/derham/">DE RHAM</a></li></ol></div><div class="macro__col"><h3 id="homotopy"><b>HOMOTOPY</b></h3><ol><li><a href="https://anders.groupoid.space/mathematics/homotopy/coequalizer/">COEQUALIZER</a></li><li><a href="https://anders.groupoid.space/mathematics/homotopy/pushout/">PUSHOUT</a></li><li><a href="https://anders.groupoid.space/mathematics/homotopy/pullback/">PULLBACK</a></li><li><a href="https://anders.groupoid.space/mathematics/homotopy/hopf/">HOPF</a></li><li><a href="https://anders.groupoid.space/mathematics/homotopy/cw/">CW</a></li></ol></div></div></section><section><div class="macro"><div class="macro__col"><h3 id="categories"><b>CATEGORIES</b></h3><ol><li><a href="https://anders.groupoid.space/mathematics/categories/category/">CATEGORY</a></li><li><a href="https://anders.groupoid.space/mathematics/categories/functor/">FUNCTOR</a></li><li><a href="https://anders.groupoid.space/mathematics/categories/groupoid/">GROUPOID</a></li><li><a href="https://anders.groupoid.space/mathematics/categories/topos/">TOPOS</a></li><li><a href="https://anders.groupoid.space/mathematics/categories/presheaf/">PRESHEAF</a></li></ol></div></div></section><br><p>The base library for <b>cubicaltt</b> is given on separate page:
+<a href='https://anders.groupoid.space/mathematics/analysis/octo/'>𝕆</a></li></ol></div><div class="macro__col"><h3 id="algebra"><b>ALGEBRA</b></h3><ol><li><a href="https://anders.groupoid.space/mathematics/algebra/group/">GROUP</a></li><li><a href="https://anders.groupoid.space/mathematics/algebra/algebra/">ALGEBRA</a></li><li><a href="https://anders.groupoid.space/mathematics/algebra/homology/">HOMOLOGY</a></li></ol></div><div class="macro__col"><h3 id="geometry"><b>GEOMETRY</b></h3><ol><li><a href="https://anders.groupoid.space/mathematics/geometry/etale/">ETALE</a></li><li><a href="https://anders.groupoid.space/mathematics/geometry/bundle/">BUNDLE</a></li><li><a href="https://anders.groupoid.space/mathematics/geometry/manifold/">MANIFOLD</a></li><li><a href="https://anders.groupoid.space/mathematics/geometry/derham/">DE RHAM</a></li></ol></div></div></section><section><div class="macro"><div class="macro__col"><h3 id="homotopy"><b>HOMOTOPY</b></h3><ol><li><a href="https://anders.groupoid.space/mathematics/homotopy/coequalizer/">COEQUALIZER</a></li><li><a href="https://anders.groupoid.space/mathematics/homotopy/pushout/">PUSHOUT</a></li><li><a href="https://anders.groupoid.space/mathematics/homotopy/pullback/">PULLBACK</a></li><li><a href="https://anders.groupoid.space/mathematics/homotopy/hopf/">HOPF</a></li><li><a href="https://anders.groupoid.space/mathematics/homotopy/cw/">CW</a></li></ol></div><div class="macro__col"><h3 id="categories"><b>CATEGORIES</b></h3><ol><li><a href="https://anders.groupoid.space/mathematics/categories/category/">CATEGORY</a></li><li><a href="https://anders.groupoid.space/mathematics/categories/functor/">FUNCTOR</a></li><li><a href="https://anders.groupoid.space/mathematics/categories/groupoid/">GROUPOID</a></li><li><a href="https://anders.groupoid.space/mathematics/categories/topos/">TOPOS</a></li><li><a href="https://anders.groupoid.space/mathematics/categories/presheaf/">PRESHEAF</a></li></ol></div></div></section><br><p>The base library for <b>cubicaltt</b> is given on separate page:
 <a href='https://groupoid.space/misc/library/'>Formal Mathematics: The Cubical Base Library</a><br>
 </p><h1>Languages</h1><p>Non-dependent languages are targets or runtimes, and dependently typed language are provers.
 </p><h2>Verification</h2><p>Theorem provers for logic, lambda encodings exploration and homotopy calculus.</p><p>05 APR 2022 &mdash; <a href='https://alonzo.groupoid.space/'>Alonzo: STLC</a><br>

index.pug

@@ -212,6 +212,9 @@ block content
                             li: a(href='https://anders.groupoid.space/mathematics/geometry/manifold/') MANIFOLD
                             li: a(href='https://anders.groupoid.space/mathematics/geometry/derham/') DE RHAM
 
+
+            section
+                .macro
                     .macro__col
                         h3#homotopy <b>HOMOTOPY</b>
                         ol
@@ -221,8 +224,6 @@ block content
                             li: a(href='https://anders.groupoid.space/mathematics/homotopy/hopf/') HOPF
                             li: a(href='https://anders.groupoid.space/mathematics/homotopy/cw/') CW
 
-            section
-                .macro
                     .macro__col
                         h3#categories <b>CATEGORIES</b>
                         ol