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.


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
  2. Functors, Adjunctions
  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


  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 for Anders theorem prover consists of two parts Foundations and Mathematics just as HoTT Book.


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


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

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


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


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

10 OCT 2016 — Henk: Pure CoC Type System
19 JAN 2020 — Bertrand: Metamath System
26 JAN 2022 — Anders: Modal Homotopy Type System
05 APR 2022 — Alonzo: STLC Type System
02 JUN 2022 — Per: MLTT Type System


Runtimes and effect type systems.

31 DEC 2016 — Certified CPS Interpreter
31 DEC 2016 — Intercore SMP Protocol
10 OCT 2016 — Effect Type System
10 OCT 2016 — Array Processing Language

Lecture Notes

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

Issue I: Internalizing MLTT
Issue III: Homotopy Type Theory
Issue VIII: Formal Set Topos
Addendum I: Pure Type System
Addendum II: Many Faces of Equality

Groupoid Infinity granted Internship Program.
Groupoid Infinity is opening Applied Math Institute.