GROUPOЇD

Groupoid Infinity Institute is doing formalization of mathematics in the formal programming language called Anders 1.3.0, a CCHM/HTS variant of cubical type systems.

# MATHEMATICS

Mathematical theories, models and languages.

### Algebraic Systems

1. Algebraic structure
2. Group, Subgroup
3. Normal Group
4. Factorgroup
5. Abelian Group
6. Ring
7. Module
8. Field Theory
9. Linear Algebra
10. Lie, Leibniz Algebra

### (Co)Homotopy Theory

1. Pullback
2. Pushout
3. Limit, Fiber
4. Suspension, Loop
5. Smash, Wedge, Join
6. H-(co)spaces
7. Eilenberg-MacLane Spaces
8. Cell Complexes
9. (Co)Homotopy
10. Hopf Invariant

### (Co)Homology Theory

1. Chain Complex
2. (Co)Homology
3. Stinrod Axioms
4. Hom and Tensor
5. Resolutions
6. Derived Cat, Fun
7. Tor, Ext and Local Cohomology
8. Homological Algebra
9. Cohomology Operations

### Category Theory

1. Categories
3. Natural Transformations
4. Kan Extensions
5. (Co)limits
6. Universal Properties
7. Structure Identity Principle

### Topos Theory

1. Topology
2. Coverings
3. Grothendieck Topology
4. Grothendieck Topos
5. Geometric Morphisms
6. Elementary Topos

### Geometry

1. Nisnevich Site
2. Zariski Site
3. Theory of Schemes
4. Noetherian Scheme
5. A¹-Homotopy Theory
6. Cohesive Topos
7. Etale Topos
8. Local Homotopy Theory

# HOMOTOPY LIBRARY

Homotopy Library for Anders theorem prover consists of two parts Foundations and Mathematics just as HoTT Book.

## Foundations

MLTT, Modal and Univalent Foundations represent a basic language primitives of Anders and its base library.

1. Π, Σ, =
2. 0, 1, 2, W
3. +, 1+
4. N, LIST
5. FIN, VEC

## Mathematics

The second part is dedicated to mathematical models and theories internalized in this language.

### TOPOI

The base library for cubicaltt is given on separate page: Formal Mathematics: The Cubical Base Library

# Languages

Non-dependent languages are targets or runtimes, and dependently typed language are provers.

## Verification

Theorem provers for logic, lambda encodings exploration and homotopy calculus.

19 JAN 2010 — Bertrand: Metamath
05 APR 2022 — Alonzo: STLC
10 OCT 2016 — Henk: System Pω
02 JUN 2022 — Per: MLTT
26 JAN 2022 — Anders: Modal HoTT

## Runtime

Runtimes and effect type systems.

31 DEC 2016 — Certified CPS
31 DEC 2016 — Intercore MP
10 OCT 2016 — Effects IOI/IO
10 OCT 2016 — Formal Tensor FTL

# Lecture Notes

The series of articles on foundation and mathematics of Homotopy Type Theory.

Groupoid Infinity is opening Applied Math Institute.