| Autor(es) | Vladimir Voevodsky (1966–2017); Steve Awodey; Michael Warren; Thierry Coquand |
| Fecha / periodo | 2009–2013 · Siglo XXI · Estados Unidos |
| Tipo | Formal |
| Deriva de | Lógica categórica y de topos · Teoría de tipos de Martin-Löf y correspondencia Curry–Howard · Cálculo de construcciones y asistentes de prueba |
| Derivan de ella | — |
| Tres leyes | Identidad: ✓ y ampliada (la igualdad es un tipo con estructura: caminos, caminos entre caminos) · No contradicción: ✓ (\(\neg(A \times \neg A)\) es habitable) · Tercio excluso: matizado (compatible con la univalencia para proposiciones; refutado por ella para todos los tipos) |
La teoría homotópica de tipos (HoTT) parte de una observación sobre la teoría intensional de Martin-Löf: el tipo de identidad \(a =_A b\) no se comporta como una relación que vale o no vale, sino como un espacio de «maneras de ser iguales». Si se lee cada tipo como un espacio topológico (con más precisión, un \(\infty\)-grupoide), cada prueba de \(a = b\) es un camino de \(a\) a \(b\), cada prueba de igualdad entre caminos es una homotopía, y así sucesivamente. El gesto distintivo de Voevodsky fue añadir el axioma de univalencia, que identifica la igualdad entre tipos con la equivalencia entre ellos. El resultado es un fundamento de la matemática en el que las estructuras isomorfas son literalmente iguales, lo que la práctica matemática ya suponía de modo informal, y que está pensado para comprobarse en ordenador.
Base. La teoría de tipos dependientes intensional de Martin-Löf: tipos \(\Pi\) (funciones dependientes), \(\Sigma\) (pares dependientes), coproductos \(A + B\), tipos \(\mathbf{0}\) y \(\mathbf{1}\), naturales, y una jerarquía de universos \(\mathcal{U}_0 : \mathcal{U}_1 : \dots\). Las proposiciones son tipos y sus pruebas, habitantes (Curry–Howard). \(\neg A\) abrevia \(A \to \mathbf{0}\).
Tipos de identidad.
De \(J\) se derivan la simetría (inversión de caminos), la transitividad (composición), el transporte (\(p : x = y\) y \(u : P(x)\) dan \(p_*(u) : P(y)\)) y la acción de funciones sobre caminos (\(\mathsf{ap}_f\)). Las leyes de grupoide valen solo salvo caminos superiores.
Modelos previos. Hofmann y Streicher (1994, publicado en 1998) construyeron un modelo en grupoides en el que la «unicidad de las pruebas de identidad» (UIP) falla: hay tipos con dos pruebas distintas de \(a = a\). Awodey y Warren (2009) interpretaron los tipos de identidad en categorías de modelos de Quillen, es decir, en la teoría de homotopía abstracta.
Niveles de homotopía. Un tipo es contráctil si tiene un centro al que todo está unido por un camino; es una proposición si dos elementos cualesquiera son iguales; es un conjunto si dos caminos paralelos cualesquiera son iguales; es un 1-grupoide si lo son dos homotopías paralelas; y así en adelante. La lógica usual vive en el nivel de las proposiciones.
Axioma de univalencia. Para tipos \(A, B : \mathcal{U}\), la función canónica \(\mathsf{idtoeqv} : (A =_{\mathcal{U}} B) \to (A \simeq B)\) es una equivalencia. Informalmente: \((A = B) \simeq (A \simeq B)\). Consecuencias:
Tipos inductivos superiores. Se generan por constructores de puntos y de caminos. El círculo \(S^1\) tiene un punto \(\mathsf{base}\) y un camino \(\mathsf{loop} : \mathsf{base} = \mathsf{base}\). Se prueba en la propia teoría que el grupo fundamental del círculo es \(\mathbb{Z}\) (Licata y Shulman, 2013). El truncamiento proposicional \(\lVert A \rVert\) convierte un tipo en una proposición y permite definir la disyunción y el existencial «a la manera lógica», sin retener el testigo.
Lógica y tercio excluso. Hay dos versiones. \(\mathsf{LEM}_{-1}\): para toda proposición \(P\), \(P + \neg P\). Es consistente con la univalencia y puede añadirse como axioma. \(\mathsf{LEM}_\infty\): para todo tipo \(A\), \(A + \neg A\). El libro de HoTT demuestra que es incompatible con la univalencia (corolario 3.2.7, a partir del teorema 3.2.2 sobre la doble negación), porque elegiría uniformemente un elemento de cada tipo, y eso no es invariante por la autoequivalencia no trivial de \(\mathbf{2}\). Lo mismo ocurre con el axioma de elección: su versión para conjuntos es consistente; la versión sin truncar, no.
Metateoría. Voevodsky dio un modelo en conjuntos simpliciales (publicado por Kapulkin y Lumsdaine en 2021), que muestra la consistencia de la univalencia respecto de ZFC con universos. La univalencia, formulada como axioma, bloquea la computación: un término cerrado de tipo \(\mathbb{N}\) puede no reducirse a un numeral. La teoría de tipos cúbica (Cohen, Coquand, Huber y Mörtberg, 2018) da a la univalencia contenido computacional.
HoTT procede de la teoría de tipos de Martin-Löf, cuya versión intensional reinterpreta homotópicamente: la regla \(J\) y los tipos de identidad son de Martin-Löf; la lectura de sus modelos como espacios es nueva. De la lógica categórica recibe el método: los modelos de grupoides de Hofmann y Streicher y los modelos en categorías de modelos de Awodey y Warren son construcciones categóricas, y la semántica prevista de HoTT son los \((\infty,1)\)-topos. Del cálculo de construcciones y sus asistentes recibe el entorno de trabajo: Voevodsky desarrolló su biblioteca Foundations, luego UniMath, en Coq a partir de 2010, y la formalización ha acompañado al programa desde el principio.
El programa se sistematizó durante el año especial del Institute for Advanced Study (2012–2013), del que salió el libro colectivo Homotopy Type Theory: Univalent Foundations of Mathematics (2013). Después se ha desarrollado en asistentes como Agda (con su modo cúbico), Coq y Lean.
Voevodsky, medallista Fields en 2002, llegó a los fundamentos por una razón práctica: había encontrado errores en trabajos propios y ajenos y quería que la matemática pudiera verificarse mecánicamente. HoTT compite con la teoría de conjuntos como fundamento, no en potencia, sino en naturalidad: en ZFC un grupo es un conjunto con una estructura, y dos grupos isomorfos son objetos distintos; en HoTT son iguales. Para la pregunta «¿una lógica o muchas?» el caso es notable. La lógica interna es intuicionista por defecto, pero admite el tercio excluso para proposiciones y lo prohíbe para tipos de nivel superior: la validez de un mismo principio depende del nivel de homotopía al que se aplique. Además, la noción de identidad, que las lógicas tradicionales daban por primitiva y trivial, se convierte en objeto de estudio con estructura propia.