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

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. PROCESS
  2. INFINITESIMAL
  3. LOCALIZATION

UNIVALENT

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

MATHEMATICS

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

ANALYSIS

  1. TOPOLOGY
  2. SET
  3. ℚ, ℝ
  4. ℂ, ℍ, 𝕆

ALGEBRA

  1. GROUP
  2. ALGEBRA
  3. HOMOLOGY

GEOMETRY

  1. ETALE
  2. BUNDLE
  3. MANIFOLD
  4. DE RHAM

HOMOTOPY

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

CATEGORIES

  1. CATEGORY
  2. FUNCTOR
  3. GROUPOID
  4. TOPOS
  5. PRESHEAF

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

LECTURES

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


🧊