L'Infini des Groupoïdes
L'Infini des Groupoïdes accomplit une synthèse monumentale, unifiant les mathématiques synthétiques et classiques dans un cadre mécaniquement vérifiable, AXIO/1, démontrant sa capacité à englober les domaines algébrique, analytique, géométrique, catégorique, topologique et fondamental à travers un ensemble de langages : Anders (HoTT cubique), Dan (HoTT simplicial), Jack (K-théorie, fibrations de Hopf), Urs (supergéométrie), Fabien (HoTT A1). Ses constructeurs de types — couvrant les ∞-catégories simpliciales, les spectres stables, les modalités cohésives, les réels, ZFC, les grands cardinaux et le forcing — en font une œuvre d'une beauté infinie.