forked from groupoid/groupoid.space
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathindex.html
More file actions
21 lines (20 loc) · 2.85 KB
/
index.html
File metadata and controls
21 lines (20 loc) · 2.85 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
<!DOCTYPE html><html><head><meta charset="utf-8"><meta http-equiv="x-ua-compatible" content="ie=edge"><meta name="viewport" content="width=device-width, initial-scale=1"><meta name="author" content="Maxim Sokhatsky"><meta name="twitter:site" content="@5HT"><meta name="twitter:creator" content="@5HT"><meta property="og:title" content="GROUPOЇD"><meta property="og:description" content="NOTES"><meta property="og:type" content="website"><meta property="fb:app_id" content="118554188236439"><meta property="og:url" content="https://groupoid.space"><link rel="stylesheet" href="https://groupoid.space/main.css?v=6"><title>GROUPOЇD</title></head><body class="content"></body></html><nav><a href='https://etale.space'>ÉTALE</a>
<a href='https://sheaf.space'>SHEAF</a>
<a href='https://groupoid.space'>GROUPOЇD</a></nav><article class="main"><div class="om"><section><h1>Foundations</h1><p>The series of notes about MLTT and Foundations.</p><p>10 OCT 2016 — <a href='https://phd.5ht.co/pts/pure/index.html'>Pure Type System</a><br>
3 AUG 2017 — <a href='mltt/types/index.html'>Math Components</a><br>
19 OCT 2017 — <a href='https://phd.5ht.co/mltt/inductive/index.html'>Recursion Schemes</a><br>
</p><h1>Homotopy Theory</h1><p>The series of notes on Homotopy Type Theory.</p><p>10 OCT 2017 — <a href='mltt/iso/index.html'>Isomorphism</a><br>
30 DEC 2018 — <a href='mltt/equiv/index.html'>Equivalence</a><br>
20 JUN 2017 — <a href='mltt/hopf/index.html'>Hopf Fibrations</a><br>
</p><h1>Base Library</h1><p>The examples of base library man pages.</p><p>16 JUL 2017 — <a href='mltt/types/pi/index.html'>Pi</a><br>
5 NOV 2017 — <a href='mltt/types/category/index.html'>Category</a><br>
20 MAY 2018 — <a href='mltt/types/bundle/index.html'>Bundle</a><br>
25 JUL 2018 — <a href='mltt/types/path/index.html'>Path</a><br>
25 JUL 2018 — <a href='mltt/types/cw/index.html'>CW Complex</a><br>
22 JAN 2019 — <a href='mltt/types/homology/index.html'>Homology</a><br>
</p><h1>Articles</h1><p>The series of articles on foundation and mathematics of Homotopy Type Theory.</p><p>— <a href='tex/articles/mltt/mltt.pdf'>Issue I: Internalizing MLTT</a><br>
— <a href='tex/articles/hott/hott.pdf'>Issue III: Homotopy Type Theory</a><br>
— <a href='tex/articles/topos/topos.pdf'>Issue VIII: Formal Set Topos</a><br>
— <a href='tex/articles/pts/pts.pdf'>Addendum I: Pure Type System</a><br>
— <a href='tex/articles/equ/equ.pdf'>Addendum II: Many Faces of Equality</a><br>
</p></section></div></article><footer class="footer"><a href="https://tonpa.guru/"><img class="footer__logo" src="https://longchenpa.guru/seal.png" width="50"></a><span class="footer__copy">2016—2019 © <a href="https://groupoid.space/" style="color:Lavender;">Groupoid Infinity</a></span><script src="https://groupoid.space/highlight.js"></script></footer>