GROUPOЇD

Groupoid Infinity 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.



The process of creating laboratory artifacts:

MATHEMATICS

First, we pick up one topic from known mathematical theories:



    Algebraic Systems

  1. Algebraic Structure
  2. Group, Subgroup
  3. Normal Group
  4. Factorgroup
  5. Abelian Group
  6. Ring, Module
  7. Simple Finite Groups
  8. Field Theory
  9. Linear Algebra
  10. Universal Algebra
  11. 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. Cohesive Topos
  8. Etale Topos
  9. Elementary Topos

    Geometry

  1. Nisnevich Site
  2. Zariski Site
  3. Theory of Schemes
  4. Noetherian Scheme
  5. A¹-Homotopy Theory
  6. Differential Geometry
  7. Synthetic Geometry
  8. Local Homotopy Theory


    Analysis

  1. Real Analysis
  2. Funtional Analysis
  3. Hilbert Space
  4. Lebesgue Integral
  5. Bochner Integral
  6. Fredholm Operators
  7. Theory of Distributions
  8. 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

Second, we formalize this theory in one of the mathematical languages best suited for that theory:

Foundations

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

Third, we publish this as an article for peer review and include in series of articles on foundation, systems, languages and mathematics in Quantum Super Stable Simplicial Modal Local Homotopy Type Theory with General Higher Induction:



    Foundations

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

    Languages

  1. Alonso Church
  2. Felix Bloch
  3. Joe Armstrong
  4. Robin Milner
  5. Yves Lafont
  6. Henk Barendregt
  7. Frank Pfenning
  8. Anders Mörtberg
  9. Laurent Schwartz
  10. Urs Schreiber

    Mathematics

  1. Algebra vs Geometry
  2. Category Theory
  3. Topos Theory
  4. Categories with Families
  5. Categories with Representable Maps
  6. Abelian Categories
  7. Comprehension Categories
  8. Cosmic Cube
  9. Fibered Categories
  10. Chevalley Descent
  11. Local Cartesian Closed Categories
  12. Symmetric Monoidal Categories
  13. Cohesive Topoi
  14. Quillen Model Structure
  15. Grothendieck Schemes
  16. Simplicial Homotopy Theory
  17. Cohomology and Spectra
  18. Grothendieck Yoga


Books:

Volume I establishes common preliminary foundations: 1) Martin-Löf Type Theory for set valued mathematics; and 2) Homotopy Type Theory for higher groupoid valued mathematics.


  Volume I: Foundations

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

Volume III coutains articles dedicated to synthetical 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