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 Structure
- Group, Subgroup
- Normal Group
- Factorgroup
- Abelian Group
- Ring, Module
- Simple Finite Groups
- Field Theory
- Linear Algebra
- Universal Algebra
- Lie, Leibniz Algebra
Algebraic Systems
- Pullback
- Pushout
- Limit, Fiber
- Suspension, Loop
- Smash, Wedge, Join
- H-(co)spaces
- Eilenberg-MacLane Spaces
- Cell Complexes
- ∞-Groupoids
- (Co)Homotopy
- Hopf Invariant
(Co)Homotopy Theory
- Chain Complex
- (Co)Homology
- Stinrod Axioms
- Hom and Tensor
- Resolutions
- Derived Cat, Fun
- Tor, Ext and Local Cohomology
- Homological Algebra
- Spectral Sequences
- Cohomology Operations
(Co)Homology Theory
- Categories
- Functors, Adjunctions
- Natural Transformations
- Kan Extensions
- (Co)limits
- Universal Properties
- Monoidal Categories
- Enriched Categories
- Structure Identity Principle
Category Theory
- Topology
- Coverings
- Grothendieck Topology
- Grothendieck Topos
- Geometric Morphisms
- Higher Topos Theory
- Cohesive Topos
- Etale Topos
- Elementary Topos
Topos Theory
- Nisnevich Site
- Zariski Site
- Theory of Schemes
- Noetherian Scheme
- A¹-Homotopy Theory
- Differential Geometry
- Synthetic Geometry
- Local Homotopy Theory
Geometry
- Real Analysis
- Funtional Analysis
- Hilbert Space
- Lebesgue Integral
- Bochner Integral
- Fredholm Operators
- Theory of Distributions
- Measure Theory
Analysis
- Proof Theory
- Set Theory
- Schönfinkel
- Łukasiewicz
- Frege
- Hilbert
- Church
- Tarski
Foundations
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.
Mathematics
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.
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:
- Alonzo Church
- Felix Bloch
- Joe Armstrong
- Robin Milner
- Yves Lafont
- Henk Barendregt
- Per Martin-Löf
- Frank Pfenning
- Anders Mörtberg
- Laurent Schwartz
- Urs Schreiber
Languages
- Algebra vs Geometry
- Category Theory
- Topos Theory
- Categories with Families
- Categories with Representable Maps
- Abelian Categories
- Comprehension Categories
- Cosmic Cube
- Fibered Categories
- Chevalley Descent
- Local Cartesian Closed Categories
- Symmetric Monoidal Categories
- Cohesive Topoi
- Quillen Model Structure
- Grothendieck Schemes
- Simplicial Homotopy Theory
- Cohomology and Spectra
- Grothendieck Yoga
Mathematics
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 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 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 IV provides final formalizations of mathematical theories packaged in most abstract categorical form.