cleanup book style

Author: 5HT

index.html

@@ -26,5 +26,11 @@
 <a href='https://groupoid.space/misc/library/'>Formal Mathematics: The Cubical Base Library</a><br>
 
 </p></div><div class="exe"><section></section><h1>ARTICLES</h1><p>Then we publish this as an article for peer review and include in
-series of articles on foundation and mathematics of Homotopy Type Theory.</p><br><br></div><div class="types"><div class="type"><ol class="type__col"><h3>Foundations</h3><li style="font-size:14px;"><a href="https://groupoid.space/articles/mltt/mltt.pdf">Type Theory</a></li><li style="font-size:14px;"><a href="https://groupoid.space/articles/cic/cic.pdf">Inductive Types</a></li><li style="font-size:14px;"><a href="https://groupoid.space/articles/hott/hott.pdf">Homotopy Type Theory</a></li><li style="font-size:14px;"><a href="https://groupoid.space/articles/hit/hit.pdf">Higher Inductive Types</a></li><li style="font-size:14px;"><b>Modalities</b></li></ol><ol class="type__col"><h3>Languages</h3><li style="font-size:14px;"><a href="https://groupoid.space/articles/laurent/laurent.pdf">Laurent Schwartz</a></li><li style="font-size:14px;"><b>Ernst Zermelo</b></li><li style="font-size:14px;"><b>Paul Cohen</b></li><li style="font-size:14px;"><a href="https://groupoid.space/articles/henk/henk.pdf">Henk Barendregt</a></li><li style="font-size:14px;"><b>Per Martin-Löf</b></li><li style="font-size:14px;"><b>Christine Paulin-Mohring</b></li><li style="font-size:14px;"><a href="https://groupoid.space/articles/anders/anders.pdf">Anders Mörtberg</a></li><li style="font-size:14px;"><b>Dan Kan</b></li><li style="font-size:14px;"><b>Jack Morava</b></li><li style="font-size:14px;"><a href="https://groupoid.space/articles/urs/urs.pdf">Urs Schreiber</a></li><li style="font-size:14px;"><b>Fabien Morel</b></li></ol><ol class="type__col"><h3>Mathematics</h3><li style="font-size:14px;"><a href="https://groupoid.space/articles/hom/hom.pdf">Algebra vs Geometry</a></li><li style="font-size:14px;"><b>Set Theory</b></li><li style="font-size:14px;"><b>Topos Theory</b></li><li style="font-size:14px;"><b>Simple Finite Groups</b></li><li style="font-size:14px;"><b>Categories with Families</b></li><li style="font-size:14px;"><b>Heterogeneous Equality</b></li><li style="font-size:14px;"><b>Abelian Groups</b></li><li style="font-size:14px;"><b>Abelian Categories</b></li><li style="font-size:14px;"><b>Supergeometry</b></li><li style="font-size:14px;"><b>C-Systems</b></li><li style="font-size:14px;"><b>Grothendieck Group</b></li></ol></div><br><br></div><div class="exe"><section><h1>BOOKS</h1><p>As a result, a contribution is made to Book Volumes as example of formalization in AXIO/1 formal system.</p><br><br><div style="padding-top: 8px;"><img src="https://anders.groupoid.space/images/pdf.jpg" width="35"><a href="https://groupoid.space/books/vol1/vol1.pdf">&nbsp; Volume 1: Foundations</a></div><div style="padding-top: 8px;"><img src="https://anders.groupoid.space/images/pdf.jpg" width="35"><a href="https://groupoid.space/books/vol2/vol2.pdf">&nbsp; Volume 2: Systems</a></div><div style="padding-top: 8px;"><img src="https://anders.groupoid.space/images/pdf.jpg" width="35"><a href="https://groupoid.space/books/vol3/vol3.pdf">&nbsp; Volume 3: Languages</a></div><div style="padding-top: 8px;"><img src="https://anders.groupoid.space/images/pdf.jpg" width="35"><a href="https://groupoid.space/books/vol4/vol4.pdf">&nbsp; Volume 4: Mathematics</a></div><div style="padding-top: 8px;"><img src="https://anders.groupoid.space/images/pdf.jpg" width="35"><a href="https://groupoid.space/books/axio/axio.pdf">&nbsp; Groupoid Infinity AXIO/1 Formal System (PhD Thesis)</a></div><br><br></section><center><br>🧊 <br><br><br>
+series of articles on foundation and mathematics of Homotopy Type Theory.</p><br><br></div><div class="types"><div class="type"><ol class="type__col"><h3>Foundations</h3><li style="font-size:14px;"><a href="https://groupoid.space/articles/mltt/mltt.pdf">Type Theory</a></li><li style="font-size:14px;"><a href="https://groupoid.space/articles/cic/cic.pdf">Inductive Types</a></li><li style="font-size:14px;"><a href="https://groupoid.space/articles/hott/hott.pdf">Homotopy Type Theory</a></li><li style="font-size:14px;"><a href="https://groupoid.space/articles/hit/hit.pdf">Higher Inductive Types</a></li><li style="font-size:14px;"><b>Modalities</b></li></ol><ol class="type__col"><h3>Languages</h3><li style="font-size:14px;"><a href="https://groupoid.space/articles/laurent/laurent.pdf">Laurent Schwartz</a></li><li style="font-size:14px;"><b>Ernst Zermelo</b></li><li style="font-size:14px;"><b>Paul Cohen</b></li><li style="font-size:14px;"><a href="https://groupoid.space/articles/henk/henk.pdf">Henk Barendregt</a></li><li style="font-size:14px;"><b>Per Martin-Löf</b></li><li style="font-size:14px;"><b>Christine Paulin-Mohring</b></li><li style="font-size:14px;"><a href="https://groupoid.space/articles/anders/anders.pdf">Anders Mörtberg</a></li><li style="font-size:14px;"><b>Dan Kan</b></li><li style="font-size:14px;"><b>Jack Morava</b></li><li style="font-size:14px;"><a href="https://groupoid.space/articles/urs/urs.pdf">Urs Schreiber</a></li><li style="font-size:14px;"><b>Fabien Morel</b></li></ol><ol class="type__col"><h3>Mathematics</h3><li style="font-size:14px;"><a href="https://groupoid.space/articles/hom/hom.pdf">Algebra vs Geometry</a></li><li style="font-size:14px;"><b>Set Theory</b></li><li style="font-size:14px;"><b>Topos Theory</b></li><li style="font-size:14px;"><b>Simple Finite Groups</b></li><li style="font-size:14px;"><b>Categories with Families</b></li><li style="font-size:14px;"><b>Heterogeneous Equality</b></li><li style="font-size:14px;"><b>Abelian Groups</b></li><li style="font-size:14px;"><b>Abelian Categories</b></li><li style="font-size:14px;"><b>Supergeometry</b></li><li style="font-size:14px;"><b>C-Systems</b></li><li style="font-size:14px;"><b>Grothendieck Group</b></li></ol></div><br><br></div><div class="exe"><section><h1>BOOKS</h1><p>As a result, a contribution is made to Book Volumes as example
+of formalization in AXIO/1 formal system.</p><p>The two common Foundations cores are: 1) MLTT (for set valued mathematics)
+and 2) HoTT (for higher groupoid valued mathematics). Both are given in Volume I.</p><p>Formalization of Languages
+in Volume II means not only their syntax and semantics but also
+their internalizations in base libraries (foundations folders).</p><p>Systems Volume III coutains articles dedicated to operating
+systems and runtimes where languages are running as applications.</p><p>Volume IV Mathematics provides final formalizations of
+mathematical theories.</p><br><br><div style="padding-top: 8px;"><img src="https://anders.groupoid.space/images/pdf.jpg" width="35"><a href="https://groupoid.space/books/vol1/vol1.pdf">&nbsp; Volume 1: Foundations</a></div><div style="padding-top: 8px;"><img src="https://anders.groupoid.space/images/pdf.jpg" width="35"><a href="https://groupoid.space/books/vol2/vol2.pdf">&nbsp; Volume 2: Systems</a></div><div style="padding-top: 8px;"><img src="https://anders.groupoid.space/images/pdf.jpg" width="35"><a href="https://groupoid.space/books/vol3/vol3.pdf">&nbsp; Volume 3: Languages</a></div><div style="padding-top: 8px;"><img src="https://anders.groupoid.space/images/pdf.jpg" width="35"><a href="https://groupoid.space/books/vol4/vol4.pdf">&nbsp; Volume 4: Mathematics</a></div><div style="padding-top: 8px;"><img src="https://anders.groupoid.space/images/pdf.jpg" width="35"><a href="https://groupoid.space/books/axio/axio.pdf">&nbsp; Groupoid Infinity AXIO/1 Formal System (PhD Thesis)</a></div><br><br></section><center><br>🧊 <br><br><br>
 </center></div></article><hr><link rel="stylesheet" href="https://groupoid.space/main.css"><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 rel="me" href="https://mathstodon.xyz/@5ht" style="color:white;"><u>Максим Сохацький</u></a></span><script src="https://groupoid.space/highlight.js?v=1"></script><script src="https://groupoid.space/bundle.js"></script></footer>

index.pug

@@ -372,7 +372,21 @@ block content
 
                 h1 BOOKS
                 p.
-                    As a result, a contribution is made to Book Volumes as example of formalization in AXIO/1 formal system.
+                    As a result, a contribution is made to Book Volumes as example
+                    of formalization in AXIO/1 formal system.
+                p.
+                    The two common Foundations cores are: 1) MLTT (for set valued mathematics)
+                    and 2) HoTT (for higher groupoid valued mathematics). Both are given in Volume I.
+                p.
+                    Formalization of Languages
+                    in Volume II means not only their syntax and semantics but also
+                    their internalizations in base libraries (foundations folders).
+                p.
+                    Systems Volume III coutains articles dedicated to operating
+                    systems and runtimes where languages are running as applications.
+                p.
+                    Volume IV Mathematics provides final formalizations of
+                    mathematical theories.
                 br
                 br
                 div(style="padding-top: 8px;")