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.



MATHEMATICS

Mathematical theories, models and languages.



    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

ARTICLES

The 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

  Volume 1: Foundations
  Volume 3: Languages

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


🧊