GROUPOЇD

L'Infini des Groupoïdes achieves a landmark synthesis, unifying synthetic and classical mathematics in a mechanically verifiable framework AXIO/1 showcasing its ability to span algebraic, analytic, geometric, categorical, topological, and foundational domains in the set of languages: Anders (Cubical HoTT), Dan (Simplicial HoTT), Jack (K-Theory, Hopf Fibrations), Urs (Supergeometry), Fabien (A¹ HoTT). Its type formers—spanning simplicial ∞-categories, stable spectra, cohesive modalities, reals, ZFC, large cardinals, and forcing.



Here we will briefly describe the process of creating laboratory artifacts.

MATHEMATICS

First we pick up one topic from known mathematical theories, models and languages that has following index:



    Algebraic Systems

  1. Algebraic structure
  2. Group, Subgroup
  3. Normal Group
  4. Factorgroup
  5. Abelian Group
  6. Ring, Module
  7. Field Theory
  8. Linear Algebra
  9. Universal 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. ∞-Groupoids
  10. (Co)Homotopy
  11. 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. Spectral Sequences
  10. Cohomology Operations


    Category Theory

  1. Categories
  2. Functors, Adjunctions
  3. Natural Transformations
  4. Kan Extensions
  5. (Co)limits
  6. Universal Properties
  7. Monoidal Categories
  8. Enriched Categories
  9. Structure Identity Principle

    Topos Theory

  1. Topology
  2. Coverings
  3. Grothendieck Topology
  4. Grothendieck Topos
  5. Geometric Morphisms
  6. Higher Topos Theory
  7. 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. Differential Geometry
  9. Synthetic Geometry
  10. Local Homotopy Theory


    Analysis

  1. Real Analysis
  2. Funtional analysis
  3. Measure theory

    Foundations

  1. Proof Theory
  2. Set Theory
  3. Schönfinkel
  4. Łukasiewicz
  5. Frege
  6. Hilbert
  7. Church
  8. Tarski

    Type Theory

  1. Laurent Schwartz
  2. Ernst Zermelo
  3. Paul Cohen
  4. Henk Barendregt
  5. Per Martin-Löf
  6. Christine Paulin-Mohring
  7. Anders Mörtberg
  8. Dan Kan
  9. Jack Morava
  10. Urs Schreiber
  11. Fabien Morel

LIBRARY

Then we formalize this theory in one of mathematical language best suited for that theory.

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. Pi
  2. Sigma
  3. Id
  4. 0, 1, 2, W
  5. Nat
  6. List
  7. Fin
  8. Vec

    Univalent

  1. Path
  2. Glue
  3. Equiv
  4. Homotopy
  5. Isomorphism

    Modal

  1. Process
  2. Infinitesimal
  3. Modality
  4. Localization

Mathematics

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



    Analysis

  1. Topology
  2. Set
  3. ℚ
  4. ℝ
  5. ℂ
  6. ℍ
  7. 𝕆

    Algebra

  1. Group
  2. Field
  3. Ring
  4. Homology

    Geometry

  1. Bundle
  2. Etale
  3. Manifold
  4. de Rham

    Homotopy

  1. Coeq
  2. Pushout
  3. Pullback
  4. Hopf
  5. CW

    Categories

  1. Category
  2. Functor
  3. Adjoint
  4. Groupoid
  5. Topos
  6. Presheaf
  7. Sheaf
  8. Stack

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

ARTICLES

Then we publish this as an article for peer review and include in series of articles on foundation and mathematics of Homotopy Type Theory.



    Foundations

  1. Type Theory
  2. Inductive Types
  3. Homotopy Type Theory
  4. Higher Inductive Types
  5. Modalities

    Languages

  1. Laurent Schwartz
  2. Ernst Zermelo
  3. Paul Cohen
  4. Henk Barendregt
  5. Per Martin-Löf
  6. Christine Paulin-Mohring
  7. Anders Mörtberg
  8. Dan Kan
  9. Jack Morava
  10. Urs Schreiber
  11. Fabien Morel

    Mathematics

  1. Algebra vs Geometry
  2. Set Theory
  3. Topos Theory
  4. Simple Finite Groups
  5. Categories with Families
  6. Heterogeneous Equality
  7. Abelian Groups
  8. Abelian Categories
  9. Supergeometry
  10. C-Systems
  11. Grothendieck Group


BOOKS

As a result, a contribution is made to Book Volumes as example of formalization in AXIO/1 formal system. The two common Foundations cores are: 1) MLTT (for set valued mathematics) and 2) HoTT (for higher groupoid valued mathematics). Both are given in Volume I.


  Volume I: Foundations

The Volume II coutains articles dedicated to operating systems and runtimes where languages are running as applications. Two basic models of computations are considered: internal languages of cartesian closed categories and symmetric monoidal categories.


  Volume II: Systems

Systems Volume III coutains articles dedicated to mathematical languages designed to be optimal at proving theorems from specific mathematics. Formalization of languages, their syntax and semantics are given along with their base libraries (foundations folders).


  Volume III: Languages

Volume IV provides final formalizations of mathematical theories packaged in most abstract categorical form.


  Volume IV: Mathematics


🧊