Skip to content

Commit 3191b2b

Browse files
committed
volume 4 articles
1 parent 30e5b52 commit 3191b2b

File tree

3 files changed

+20
-12
lines changed

3 files changed

+20
-12
lines changed

books/vol4/id.pdf

199 KB
Binary file not shown.

index.html

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@
2626
<a href='https://groupoid.space/misc/library/'>Formal Mathematics: The Cubical Base Library</a><br>
2727

2828
</p></div><div class="exe"><section></section><h1>ARTICLES</h1><p>Then we publish this as an article for peer review and include in
29-
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
29+
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/books/vol4/spt.pdf">Algebra vs Geometry</a></li><li style="font-size:14px;"><a href="https://groupoid.space/books/vol4/topos.pdf">Topos Theory</a></li><li style="font-size:14px;"><a href="https://groupoid.space/books/vol4/cwf.pdf">Categories with Families</a></li><li style="font-size:14px;"><a href="https://groupoid.space/books/vol4/cwr.pdf">Categories with Reprepresentable Maps</a></li><li style="font-size:14px;"><a href="https://groupoid.space/books/vol4/id.pdf">Heterogeneous Equality</a></li><li style="font-size:14px;"><a href="https://groupoid.space/books/vol4/abelian.pdf">Abelian Groups</a></li><li style="font-size:14px;"><a href="https://groupoid.space/books/vol4/comprehension.pdf">Comprehension Categories</a></li><li style="font-size:14px;"><a href="https://groupoid.space/books/vol4/cube.pdf">Cosmic Cube</a></li><li style="font-size:14px;"><a href="https://groupoid.space/books/vol4/fibered.pdf">Fibered Categories</a></li><li style="font-size:14px;"><a href="https://groupoid.space/books/vol4/jean.pdf">Chevalley Descent</a></li><li style="font-size:14px;"><a href="https://groupoid.space/books/vol4/lccc.pdf">Local Cartesian Closed Categories</a></li><li style="font-size:14px;"><a href="https://groupoid.space/books/vol4/smc.pdf">Symmetric Monoidal Categories</a></li><li style="font-size:14px;"><a href="https://groupoid.space/books/vol4/modal.pdf">Cohesive Topoi</a></li><li style="font-size:14px;"><a href="https://groupoid.space/books/vol4/quillen.pdf">Quillen Model Structure</a></li><li style="font-size:14px;"><a href="https://groupoid.space/books/vol4/scheme.pdf">Grothendieck Schemes</a></li><li style="font-size:14px;"><a href="https://groupoid.space/books/vol4/simplicial.pdf">Simplicial Homotopy Theory</a></li><li style="font-size:14px;"><a href="https://groupoid.space/books/vol4/stable.pdf">Cohomology and Spectra</a></li><li style="font-size:14px;"><a href="https://groupoid.space/books/vol4/yoga.pdf">Grothendieck Yoga</a></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
3030
of formalization in AXIO/1 formal system.
3131
The two common Foundations cores are: 1) MLTT (for set valued mathematics)
3232
and 2) HoTT (for higher groupoid valued mathematics). Both are given in Volume I.</p><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 I: Foundations</a></div><br><p>The Volume II coutains articles dedicated to operating

index.pug

Lines changed: 19 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -341,17 +341,25 @@ block content
341341
'Urs Schreiber': 'https://groupoid.space/articles/urs/urs.pdf',
342342
'Fabien Morel': '' },
343343
344-
'Mathematics': { 'Algebra vs Geometry': 'https://groupoid.space/articles/hom/hom.pdf',
345-
'Set Theory': '',
346-
'Topos Theory': '',
347-
'Simple Finite Groups': '',
348-
'Categories with Families': '',
349-
'Heterogeneous Equality': '',
350-
'Abelian Groups': '',
351-
'Abelian Categories': '',
352-
'Supergeometry': '',
353-
'C-Systems': '',
354-
'Grothendieck Group': '' }
344+
'Mathematics': { 'Algebra vs Geometry': 'https://groupoid.space/books/vol4/spt.pdf',
345+
'Topos Theory': 'https://groupoid.space/books/vol4/topos.pdf',
346+
'Categories with Families': 'https://groupoid.space/books/vol4/cwf.pdf',
347+
'Categories with Reprepresentable Maps': 'https://groupoid.space/books/vol4/cwr.pdf',
348+
'Heterogeneous Equality': 'https://groupoid.space/books/vol4/id.pdf',
349+
'Abelian Groups': 'https://groupoid.space/books/vol4/abelian.pdf',
350+
'Comprehension Categories': 'https://groupoid.space/books/vol4/comprehension.pdf',
351+
'Cosmic Cube': 'https://groupoid.space/books/vol4/cube.pdf',
352+
'Fibered Categories': 'https://groupoid.space/books/vol4/fibered.pdf',
353+
'Chevalley Descent': 'https://groupoid.space/books/vol4/jean.pdf',
354+
'Local Cartesian Closed Categories': 'https://groupoid.space/books/vol4/lccc.pdf',
355+
'Symmetric Monoidal Categories': 'https://groupoid.space/books/vol4/smc.pdf',
356+
'Cohesive Topoi': 'https://groupoid.space/books/vol4/modal.pdf',
357+
'Quillen Model Structure': 'https://groupoid.space/books/vol4/quillen.pdf',
358+
'Grothendieck Schemes': 'https://groupoid.space/books/vol4/scheme.pdf',
359+
'Simplicial Homotopy Theory': 'https://groupoid.space/books/vol4/simplicial.pdf',
360+
'Cohomology and Spectra': 'https://groupoid.space/books/vol4/stable.pdf',
361+
'Grothendieck Yoga': 'https://groupoid.space/books/vol4/yoga.pdf',
362+
}
355363
};
356364
357365

0 commit comments

Comments
 (0)