-
Notifications
You must be signed in to change notification settings - Fork 13
/
index.html
36 lines (36 loc) · 13.6 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
<!DOCTYPE html><html><head><meta charset="utf-8"><meta http-equiv="x-ua-compatible" content="ie=edge"><meta property="fb:app_id" content="118554188236439"><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:type" content="website"><meta property="og:image" content="https://avatars.githubusercontent.com/u/17128096?s=400&u=66a63d4cdd9625b2b4b37d724cc00fe6401e5bd8&v=4"><meta name="msapplication-TileColor" content="#ffffff"><meta name="msapplication-TileImage" content="https://anders.groupoid.space/images/ms-icon-144x144.png"><meta name="theme-color" content="#ffffff"><link rel="stylesheet" href="https://anders.groupoid.space/main.css?v=1"><link rel="apple-touch-icon" sizes="57x57" href="https://anders.groupoid.space/images/apple-icon-57x57.png"><link rel="apple-touch-icon" sizes="60x60" href="https://anders.groupoid.space/images/apple-icon-60x60.png"><link rel="apple-touch-icon" sizes="72x72" href="https://anders.groupoid.space/images/apple-icon-72x72.png"><link rel="apple-touch-icon" sizes="76x76" href="https://anders.groupoid.space/images/apple-icon-76x76.png"><link rel="apple-touch-icon" sizes="114x114" href="https://anders.groupoid.space/images/apple-icon-114x114.png"><link rel="apple-touch-icon" sizes="120x120" href="https://anders.groupoid.space/images/apple-icon-120x120.png"><link rel="apple-touch-icon" sizes="144x144" href="https://anders.groupoid.space/images/apple-icon-144x144.png"><link rel="apple-touch-icon" sizes="152x152" href="https://anders.groupoid.space/images/apple-icon-152x152.png"><link rel="apple-touch-icon" sizes="180x180" href="https://anders.groupoid.space/images//apple-icon-180x180.png"><link rel="icon" type="image/png" sizes="192x192" href="https://anders.groupoid.space/images/android-icon-192x192.png"><link rel="icon" type="image/png" sizes="32x32" href="https://anders.groupoid.space/images/favicon-32x32.png"><link rel="icon" type="image/png" sizes="96x96" href="https://anders.groupoid.space/images/favicon-96x96.png"><link rel="icon" type="image/png" sizes="16x16" href="https://anders.groupoid.space/images/favicon-16x16.png"><link rel="manifest" href="https://anders.groupoid.space/images/manifest.json"><style>svg a{fill:blue;stroke:blue}
[data-mml-node="merror"]>g{fill:red;stroke:red}
[data-mml-node="merror"]>rect[data-background]{fill:yellow;stroke:none}
[data-frame],[data-line]{stroke-width:70px;fill:none}
.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="GROUPOЇD"><meta property="og:description" content="Groupoїd Infinity"><meta property="og:url" content="https://groupoid.space/"></head></html><title>GROUPOЇD</title><article class="main"><div class="exe"><section></section><p><a href="https://groupoid.space/institute/">Groupoid Infinity Institute</a> is doing formalization of mathematics
in the formal programming language called <a href="https://anders.groupoid.space/">Anders</b>
<a href="https://opam.ocaml.org/packages/anders/">1.3.0</a>,
a CCHM/HTS variant of cubical type systems.
</p></div><br><hr size=1><br><div class="exe"><section></section><h1>MATHEMATICS</h1><p>Mathematical theories, models and languages.</p></div><div class="types"><br><br><div class="type"><ol class="type__col"><h3>Algebraic Systems</h3><li><a href="https://anders.groupoid.space/mathematics/algebra/algebra/">Algebraic structure</a></li><li><b>Group, Subgroup</b></li><li><b>Normal Group</b></li><li><b>Factorgroup</b></li><li><b>Abelian Group</b></li><li><b>Ring</b></li><li><b>Module</b></li><li><b>Field Theory</b></li><li><b>Linear Algebra</b></li><li><b>Lie, Leibniz Algebra</b></li></ol><ol class="type__col"><h3>(Co)Homotopy Theory</h3><li><a href="https://anders.groupoid.space/mathematics/homotopy/pullback/">Pullback</a></li><li><a href="https://anders.groupoid.space/mathematics/homotopy/pushout/">Pushout</a></li><li><a href="https://anders.groupoid.space/mathematics/geometry/bundle/">Limit, Fiber</a></li><li><b>Suspension, Loop</b></li><li><b>Smash, Wedge, Join</b></li><li><b>H-(co)spaces</b></li><li><b>Eilenberg-MacLane Spaces</b></li><li><b>Cell Complexes</b></li><li><b>(Co)Homotopy</b></li><li><b>Hopf Invariant</b></li></ol><ol class="type__col"><h3>(Co)Homology Theory</h3><li><b>Chain Complex</b></li><li><a href="https://anders.groupoid.space/mathematics/algebra/homology/">(Co)Homology</a></li><li><b>Stinrod Axioms</b></li><li><b>Hom and Tensor</b></li><li><b>Resolutions</b></li><li><b>Derived Cat, Fun</b></li><li><b>Tor, Ext and Local Cohomology</b></li><li><b>Homological Algebra</b></li><li><b>Cohomology Operations</b></li></ol></div><br><br><div class="type"><ol class="type__col"><h3>Category Theory</h3><li><a href="https://anders.groupoid.space/mathematics/categories/category/">Categories</a></li><li><a href="https://anders.groupoid.space/mathematics/categories/functor/">Functors, Adjunctions</a></li><li><b>Natural Transformations</b></li><li><b>Kan Extensions</b></li><li><b>(Co)limits</b></li><li><b>Universal Properties</b></li><li><b>Structure Identity Principle</b></li></ol><ol class="type__col"><h3>Topos Theory</h3><li><b>Topology</b></li><li><b>Coverings</b></li><li><a href="https://anders.groupoid.space/mathematics/topoi/topos/">Grothendieck Topology</a></li><li><b>Grothendieck Topos</b></li><li><b>Geometric Morphisms</b></li><li><b>Elementary Topos</b></li></ol><ol class="type__col"><h3>Geometry</h3><li><b>Nisnevich Site</b></li><li><b>Zariski Site</b></li><li><b>Theory of Schemes</b></li><li><b>Noetherian Scheme</b></li><li><b>A¹-Homotopy Theory</b></li><li><b>Cohesive Topos</b></li><li><b>Etale Topos</b></li><li><b>Local Homotopy Theory</b></li></ol></div><br><br><div class="type"><ol class="type__col"><h3>Categorical Models</h3><li><b>Homotopical Algebra</b></li><li><a href="https://anders.groupoid.space/mathematics/topoi/presheaf/">Presheaf Type Theory</a></li><li><a href="https://tonpa.guru/stream/2020/2020-05-03%20%D0%9C%D0%BE%D0%B4%D0%B5%D0%BB%D1%8C%D0%BD%D1%8B%D0%B5%20%D0%BA%D0%B0%D1%82%D0%B5%D0%B3%D0%BE%D1%80%D0%B8%D0%B8.htm">Set Quillen model</a></li><li><a href="https://tonpa.guru/stream/2020/2020-05-03%20%D0%9C%D0%BE%D0%B4%D0%B5%D0%BB%D1%8C%D0%BD%D1%8B%D0%B5%20%D0%BA%D0%B0%D1%82%D0%B5%D0%B3%D0%BE%D1%80%D0%B8%D0%B8.htm">Top Quillen model</a></li><li><a href="https://tonpa.guru/stream/2020/2020-05-03%20%D0%9C%D0%BE%D0%B4%D0%B5%D0%BB%D1%8C%D0%BD%D1%8B%D0%B5%20%D0%BA%D0%B0%D1%82%D0%B5%D0%B3%D0%BE%D1%80%D0%B8%D0%B8.htm">sSet Quillen model</a></li><li><a href="https://anders.groupoid.space/mathematics/topoi/presheaf/">Pi Presheaf</a></li><li><a href="https://anders.groupoid.space/mathematics/topoi/presheaf/">Sigma Presheaf</a></li><li><a href="https://anders.groupoid.space/mathematics/topoi/presheaf/">sSet Presheaf</a></li><li><a href="https://anders.groupoid.space/mathematics/topoi/presheaf/">I Presheaf</a></li></ol><ol class="type__col"><h3>Type Systems</h3><li><a href="https://bertrand.groupoid.space/">METAMATH</a></li><li><a href="https://alonzo.groupoid.space/">STLC</a></li><li><a href="https://henk.groupoid.space/">PTS</a></li><li><a href="https://anders.groupoid.space/">CCHM HTS</a></li><li><a href="https://github.com/groupoid/valery">HoTT-I</a></li></ol></div></div><div class="exe"><section></section><h1>HOMOTOPY LIBRARY</h1><p>Homotopy Library for <a href="https://anders.groupoid.space/">Anders</a>
theorem prover consists of two parts Foundations and Mathematics just
as <a href="https://homotopytypetheory.org/book/">HoTT Book</a>.
</p><h2>Foundations</h2><p>MLTT, Modal and Univalent Foundations represent a basic
language primitives of <b>Anders</b> and its base library.
</p><section><div class="macro"><div class="macro__col"><h3 id="mltt"><b>MLTT</b></h3><ol><li><a href='https://anders.groupoid.space/foundations/mltt/pi/'>Π</a>, <a href='https://anders.groupoid.space/foundations/mltt/sigma/'>Σ</a>, <a href='https://anders.groupoid.space/foundations/mltt/id/'>=</a></li><li><a href='https://anders.groupoid.space/foundations/mltt/inductive/'>0, 1, 2, W</a></li><li><a href='https://anders.groupoid.space/foundations/mltt/either/'>+</a>, <a href='https://anders.groupoid.space/foundations/mltt/maybe/'>1+</a></li><li><a href='https://anders.groupoid.space/foundations/mltt/nat/'>N</a>, <a href='https://anders.groupoid.space/foundations/mltt/list/'>LIST</a></li><li><a href='https://anders.groupoid.space/foundations/mltt/fin/'>FIN</a>, <a href='https://anders.groupoid.space/foundations/mltt/vec/'>VEC</a></li></ol></div><div class="macro__col"><h3 id="modal"><b>MODAL</b></h3><ol><li><a href="https://anders.groupoid.space/foundations/modal/derham/">DERHAM</a></li><li><a href="https://anders.groupoid.space/foundations/modal/process/">PROCESS</a></li><li><a href="https://anders.groupoid.space/foundations/modal/infinitesimal/">INFINITESIMAL</a></li></ol></div><div class="macro__col"><h3 id="univalent"><b>UNIVALENT</b></h3><ol><li><a href="https://anders.groupoid.space/foundations/univalent/equiv/">EQUIV</a></li><li><a href="https://anders.groupoid.space/foundations/univalent/iso/">ISO</a></li><li><a href="https://anders.groupoid.space/foundations/univalent/funext/">FUNEXT</a></li><li><a href="https://anders.groupoid.space/foundations/univalent/path/">PATH</a></li><li><a href="https://anders.groupoid.space/foundations/univalent/glue/">GLUE</a></li></ol></div></div></section><h2>Mathematics</h2><p>The second part is dedicated to mathematical models and theories internalized in this language.
</p><section><div class="macro"><div class="macro__col"><h3 id="algebra"><b>ALGEBRA</b></h3><ol><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></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></ol></div><div class="macro__col"><h3 id="categories"><b>TOPOI</b></h3><ol><li><a href="https://anders.groupoid.space/mathematics/topoi/topos/">TOPOS</a></li><li><a href="https://anders.groupoid.space/mathematics/topoi/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>19 JAN 2010 — <a href='https://bertrand.groupoid.space'>Bertrand: Metamath</a><br>
05 APR 2022 — <a href='https://alonzo.groupoid.space/'>Alonzo: STLC</a><br>
10 OCT 2016 — <a href='https://henk.groupoid.space/'>Henk: System P<sub>ω</sub></a><br>
02 JUN 2022 — <a href='https://per.groupoid.space/'>Per: MLTT</a><br>
26 JAN 2022 — <a href='https://anders.groupoid.space/'>Anders: Modal HoTT</a><br>
</p><h2>Runtime</h2><p>Runtimes and effect type systems.</p><p>31 DEC 2016 — <a href='runtime/cps/'>Certified CPS</a><br>
31 DEC 2016 — <a href='runtime/intercore/'>Intercore MP</a><br>
10 OCT 2016 — <a href='runtime/effects/'>Effects IOI/IO</a><br>
10 OCT 2016 — <a href='runtime/ftl/'>Formal Tensor FTL</a><br>
</p><h1>Lecture Notes</h1><p>The series of articles on foundation and mathematics of Homotopy Type Theory.</p><p>— <a href='articles/mltt/mltt.pdf'>Issue I: Internalizing MLTT</a><br>
— <a href='articles/hott/hott.pdf'>Issue III: Homotopy Type Theory</a><br>
— <a href='articles/topos/topos.pdf'>Issue VIII: Formal Set Topos</a><br>
— <a href='articles/pts/pts.pdf'>Addendum I: Pure Type System</a><br>
— <a href='articles/equ/equ.pdf'>Addendum II: Many Faces of Equality</a><br></p><p><!-- Groupoid Infinity granted <a href="https://groupoid.space/misc/internship/">Internship Program</a>. <br -->
Groupoid Infinity is opening <a href="https://groupoid.space/institute/">Applied Math Institute</a>.
</p></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">2016—2022 © <a rel="me" href="https://twiukraine.com/@5HT" style="color:Lavender;">Namdak Tönpa</a></span><script src="https://groupoid.space/highlight.js"></script><script src="https://groupoid.space/bundle.js"></script></footer>