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
  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

    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


    Categorical Models

  1. Homotopical Algebra
  2. Presheaf Type Theory
  3. Set Quillen model
  4. Top Quillen model
  5. sSet Quillen model
  6. Pi Presheaf
  7. Sigma Presheaf
  8. sSet Presheaf
  9. I Presheaf

    Type Systems

  1. METAMATH
  2. STLC
  3. PTS
  4. CCHM HTS
  5. HoTT-I

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.

MLTT

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

UNIVALENT

  1. EQUIV
  2. ISO
  3. FUNEXT
  4. PATH
  5. GLUE

Mathematics

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

ALGEBRA

  1. ALGEBRA
  2. HOMOLOGY

GEOMETRY

  1. ETALE
  2. BUNDLE
  3. MANIFOLD

HOMOTOPY

  1. COEQUALIZER
  2. PUSHOUT
  3. PULLBACK
  4. HOPF
  5. CW

CATEGORIES

  1. CATEGORY
  2. FUNCTOR
  3. GROUPOID

TOPOI

  1. TOPOS
  2. PRESHEAF

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.

— 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 is opening Applied Math Institute.