¿Cómo citar este artículo?

Contreras, C. (2026). Teoría Homotópica de Tipos I: Introducción a los Fundamentos Univalentes. Revista de Filosofía Homónima, 1(2), pp. 281-307

Constantino Contreras 

 

En este artículo, el primero de una bilogía, se introduce al lector no especializado a la Teoría Homotópica de Tipos (HoTT), un reciente marco fundacional para las matemáticas donde convergen lógica, computación, topología y teoría de tipos. En la segunda parte, varias de las aplicaciones e implicaciones filosóficas de HoTT serán exploradas.

Introducción

La teoría homotópica de tipos (HoTT, por sus siglas en inglés) es un programa de investigación reciente propuesto como un nuevo “lenguaje fundacional para las matemáticas” (The Univalent Foundations Program 2013, p. 17). Formalmente, es indiscutible que HoTT consigue este objetivo: tanto la teoría de conjuntos, la teoría de categorías y otras teorías avanzadas pueden subsumirse dentro de su lenguaje. Todas las matemáticas pueden realizarse dentro de HoTT. Además de su estatus como fundamento para las matemáticas, ha ganado notoriedad por otras cualidades interesantes: la implementación de lenguajes de programación (como Lean o Rocq) basados en su teoría de tipos para asistir y realizar demostraciones matemáticas, su lógica interna no clásica, su fundamentación tanto de las matemáticas clásicas como constructivas e intuicionistas, su tratamiento no estándar y enriquecido de la identidad, nuevos axiomas para la práctica matemática entre otras.

Para el matemático interesado en fundamentos, HoTT es una teoría tan indispensable como la teoría de conjuntos o la teoría de categorías. Para el filósofo, HoTT presenta varias cuestiones interesantes. ¿Cómo debemos interpretar la ontología, la epistemología y la práctica matemática a la luz de este nuevo fundamento? A pesar de ser un fundamento para las matemáticas, su propia teoría presupone muchas matemáticas avanzadas que, en principio, debería fundamentar: ¿será posible hacer que HoTT sea un fundamento autónomo, independiente de otras teorías previas? (Ladyman & Presnell, 2016; Tsementzis, 2020). HoTT también puede usarse, por ejemplo, para formalizar el estructuralismo matemático (Awodey 1996; Tsementzis 2017). Para el filósofo de la ciencia, HoTT incluso podría formalizar algunos aspectos del realismo estructural óntico (Chen, 2024), o resolver problemas de la física y metafísica de la relatividad general (Ladyman & Presnell, 2020). Para el metafísico, el novedoso tratamiento de la identidad en HoTT podría resolver problemas filosóficos no tratados por las nociones más tradicionales de la lógica clásica (Rodin, 2024). En fin, es indudable que HoTT trae consigo un nuevo paradigma tanto matemático como filosófico que no debería pasar desapercibido.

El objetivo de la siguiente serie de dos artículos, siendo esta su primera instancia, es lograr precisamente esto. En tanto no existe, de momento, literatura en español acerca de la teoría homotópica de tipos, ni de sus problemáticas filosóficas, la presente serie de artículos pretende llenar tal vacío. En esta primera parte nos dedicaremos a introducir la teoría formal de HoTT necesaria para las discusiones filosóficas mencionadas anteriormente de una manera accesible para un lector no especializado. En la segunda parte, las discusiones filosóficas abiertas por HoTT, y su estado actual en la literatura, serán presentadas al lector.

Antes de empezar, como pequeña nota técnica, vale la pena aclarar que aunque en el título, y a lo largo del artículo, nos referimos a HoTT como fundamentos univalentes de las matemáticas, lo cierto es que la noción tiene un alcance más general. Un fundamento univalente es un marco fundacional el cual o es una teoría de tipos donde el axioma de Univalencia es cierto, o es un \((\infty,1)\)-topos con un clasificador de objetos. La teoría de topos, parte de la teoría de categorías, se ha propuesto también como un marco fundacional para las matemáticas en tanto la noción de topos generaliza y subsume la estructura de otros sistemas fundacionales, como la teoría de conjuntos o la teoría de tipos. Si bien usaremos algunas nociones categóricas, extendernos en la teoría de topos nos llevaría muy lejos del alcance de esta serie de artículos centrados, principalmente, en la teoría homotópica de tipos. Así, de aquí en adelante usaremos teoría homotópica de tipos y fundamentos univalentes intercambiablemente.

La Teoría de Tipos de Martin-Löf

Tipos, juicios y reglas

La base formal que subyace a la teoría homotópica de tipos es la teoría de tipos de Martin-Löf (MLTT, por sus siglas en inglés), desarrollada por el lógico y filósofo sueco Per Martin-Löf (1942–) a mediados de 1970 (Martin-Löf, 1975; 1998). También llamada teoría de tipos intuicionista, MLTT es una teoría de tipos dependientes que agrega tipos de identidad y tipos inductivos. ¿Pero qué es un tipo?

Una de las primeras intuiciones ofrecidas a los estudiantes primerizos de teoría de tipos es que un tipo puede verse como una especie de conjunto. Esta intuición es un punto de partida útil para nuestro primer acercamiento. Así, un tipo, como su nombre indica, puede entenderse como un conjunto de elementos u objetos que son del mismo tipo, o de la misma clase. Por ejemplo, el 0 y el 1 son ambos objetos del mismo tipo, a saber, ambos son números naturales y por tanto pertenecen al tipo de los naturales. Análogamente, \(\pi\) y \(e\) son del tipo de los irracionales, y verdad y falso ambos son valores de verdad, o del tipo de los booleanos. Los elementos de un cierto tipo se conocen como términos o tokens, y decimos que habitan su tipo. Para denotar que un término \(x\) habita el tipo \(A\) usamos la notación \(x:A\), la cual, según la interpretación conjuntista, puede leerse como \(x \in A\). Además, los términos solo pueden habitar un único tipo.

Con esto en mente, un tipo dependiente es un tipo que depende de un término de otro tipo en su definición. Por ejemplo, si tomamos un número natural \(n\mathbb{:N}\), podemos definir el tipo de vectores de longitud \(n\) cuyas entradas son números reales, \(Vect_{\mathbb{R}}(n)\). Más generalmente, dado \(x:A\), el tipo \(B(x)\) es un tipo dependiente de, o indexado por, el término \(x\). Si para todo término del tipo \(A\) hay un tipo dependiente \(B(x)\), entonces el tipo \(B\) es una familia de tipos sobre \(A\), cada término \(b(x):B(x)\) se conoce como una sección de la familia y cada \(B(x)\) se conoce como fibra de la familia, ya que en HoTT se interpretan como fibraciones, concepto que veremos a detalle en la sección 3.1. Así, el tipo \(Vect_{\mathbb{R}}\) es una familia sobre \(\mathbb{N}\), cada \(Vect_{\mathbb{R}}(n)\) es una de sus fibras y cada vector del tipo es una sección de tal familia.

Ahora, es importante recalcar el hecho de que expresiones como \(x:A\) no son proposiciones en MLTT sino juicios. Las proposiciones son tipos dentro de MLTT, mientras que un juicio como \(x:A\) no es un tipo sino una expresión en la metateoría de MLTT.¹ A diferencia de una proposición como \(x \in A\), la cual es una relación binaria en lógica de primer orden que puede ser cierta o falsa, el juicio \(x:A\) simplemente asevera que \(x\) es un elemento de \(A\), más de forma imperativa que de forma descriptiva; uno no puede refutar un juicio como \(x:A\). Este hecho es notable, porque es lo que hace que MLTT incorpore un constructivismo directamente en su teoría: los tipos y elementos se construyen y definen a partir de las reglas de MLTT. No se asume la existencia de objetos matemáticos de antemano que son luego “capturados” por nuestras definiciones (como ocurre, e.g., en ZFC); todo objeto matemático se construye y se define mediante reglas que lo especifican y caracterizan totalmente.

En MLTT tendremos los siguiente juicios:

• \(\Gamma\ \text{ctx}\) — \(\Gamma\) es un contexto,

• \(\Gamma \vdash A\ \text{type}\) — \(A\) es un tipo,

• \(\Gamma \vdash A \equiv B\ \text{type}\) — \(A\) y \(B\) son tipos definicionalmente iguales,

• \(\Gamma \vdash a:A\) — \(a\) es un término del tipo \(A\),

• \(\Gamma \vdash a \equiv b:A\) — \(a\) y \(b\) son términos definicionalmente iguales.

Primero, todo juicio \(\mathfrak{J}\) en MLTT se realiza con respecto a un contexto \(\Gamma\), denotado como \(\Gamma\mathfrak{\vdash J}\). Un contexto es una lista de declaraciones de variables

\[a_{1}:A_{1},a_{2}:A_{2}\left( a_{1} \right),\ldots,a_{n}:A_{n}\left( a_{1},\ldots,a_{n – 1} \right)\]

tal que para toda k, con \(1 \leq k \leq n\), \(A_{k}\left( a_{1},…,a_{k – 1} \right)\) es un tipo (dependiente) en el contexto definido hasta \(k – 1\). Es decir, que

\[a_{1}:A_{1},\ldots,a_{k – 1}:A_{k – 1}\left( a_{1},\ldots,a_{k – 2} \right) \vdash A_{k}\left( a_{1},\ldots,a_{k – 1} \right)\ \text{type}\]

Aquí hay tres observaciones importantes. Primero, las declaraciones de variables \(a_{i}:A_{i}\left( a_{1},\ldots,a_{i – 1} \right)\) no son juicios. Un juicio es una aserción que se hace en un cierto contexto. Aquí estamos apenas poniendo sobre la mesa las asunciones sobre las que trabajaremos. Una vez vista la interpretación de tipos como proposiciones (sección 2.2), podremos interpretar estas declaraciones de variable como los axiomas, o postulados, sobre los que trabajaremos nuestras teorías posteriores. Segundo, los \(a_{1},…,a_{n}\) declarados en contextos se conocen como términos hipotéticos o variables. De cierta forma, en nuestro contexto presuponemos que cada tipo \(A_{1},\ldots A_{n}\) está habitado por estos términos hipotéticos, sin mostrar ningún término explícito todavía. Finalmente, aunque el uso de tipos dependientes en la definición de contexto puede parecer pesada, lo único que estamos haciendo es ir definiendo sucesivamente tipos que pueden tener acceso a las variables introducidas anteriormente. Nada más. Podríamos definir, por ejemplo, un contexto más simple como \(a_{1}:A_{1},…,a_{n}:A_{n}\) sin tipos dependientes, en cuyo caso ningún tipo \(A_{i}\) tiene acceso a las variables de los tipos anteriores. Es más, hay contextos que no poseen ninguna declaración de variable, como el contexto vacío, denotado por \(\varepsilon\). De esta manera, los juicios hechos en el contexto vacío son juicios que pueden hacerse sin asumir nada de antemano, sin hipótesis, y pueden realizarse en absolutamente cualquier contexto.

Ahora, la igualdad definicional a la que refieren los otros juicios es una igualdad sintáctica, siendo así la igualdad más fuerte y estricta posible entre los objetos de la teoría de tipos. En la sección 2.2 veremos otra noción de identidad más laxa que MLTT incorpora, llamada igualdad proposicional.

Una vez vistos los juicios, usaremos ciertas reglas de inferencia para operar sobre ellos y derivar otros juicios, de manera análoga a la deducción natural. Una regla de inferencia por lo general adopta la siguiente forma (con los juicios de arriba siendo premisas y el juicio de abajo la conclusión):

 

Por ejemplo, tendremos las reglas que afirman que la igualdad definicional es una relación de equivalencia.

Con reglas análogas para la igualdad definicional de términos. Debido a que la igualdad definicional es la más fuerte de todas, podemos hacer la siguiente sustitución:

Otro tipo de sustitución que puede realizarse es a la hora de trabajar con variables (términos hipotéticos). Pensemos por ejemplo en un polinomio como \(2x^{2} + x^{3}\). Al sustituir la variable \(x\mathbb{:N}\) por un número como \(1\mathbb{:N}\) tendremos el valor \(3\). En MLTT una sustitución de este estilo tiene la forma general:

Donde \(\Delta\) es un contexto de la forma \(y_{1}:B_{1},\ldots,y_{n}:B_{n}\) y \(\mathfrak{J}\) un juicio cualquiera. Así, sustituimos simultáneamente en \(\Delta\) y \(\mathfrak{J}\) el término \(a\) por la variable \(x\). En este caso, \(\Delta\lbrack a/x\rbrack\) adquiere la forma \(y_{1}:B_{1}\lbrack a/x\rbrack,\ldots,y_{n}:B_{n}\lbrack a/x\rbrack\), por lo que los términos \(y_{1},\ldots,y_{n}\) son asignados a nuevos tipos. Nuevamente, debido a que la igualdad definicional es la más fuerte, estas podremos sustituir iguales por iguales en las sustituciones anteriores, es decir:

Aquí hacemos un poco de abuso de notación al escribir \(\mathfrak{J}\lbrack a/x\rbrack\mathfrak{\equiv J}\lbrack b/x\rbrack\), pero pretende simplificar los dos juicios siguientes: \(C\lbrack a/x\rbrack \equiv C\lbrack b/x\rbrack\ \text{type}\) y \(c\lbrack a/x\rbrack \equiv c\lbrack b/x\rbrack:C\lbrack a/x\rbrack\). Otra regla importante, la cual puede derivarse por inducción sobre estructura de cada derivación, es la regla de debilitamiento, o weakening en inglés:

Esta regla afirma que todo juicio \(\mathfrak{J}\) hecho en el contexto \(\Gamma,\Delta\) puede realizarse en el contexto extendido por \(x:A\). Otra regla importante, llamada regla de la variable, nos permite pasar de variables, o términos hipotéticos, a términos simpliciter. De esta forma, podemos materializar la presuposición realizada en un contexto de que un cierto tipo está habitado.

La regla de variable, de debilitamiento y de sustitución se agrupan en las reglas estructurales. Ahora veremos las reglas que gobiernan y caracterizan a los tipos y sus términos.

En general, caracterizamos y definiremos a todo tipo usando cuatro reglas:

• Una regla de formación que nos dice cómo construir el tipo

• Una regla de introducción que nos dice cómo construir términos de ese tipo

• Una regla de eliminación que nos dice cómo utilizar los términos del tipo

• Una regla de computación, conocida también como \(\beta\)-reducción, que nos dice cómo la regla de eliminación actúa sobre la regla de formación y nos garantizan que los términos del tipo funcionan como es esperado

Empecemos por el tipo función \(A \rightarrow B\). Su regla de introducción es clara:

Ahora, para entender el resto de sus reglas (y las de otros tipos) necesitamos entender primero el concepto de \(\lambda\)-abstracción, originalmente nativo del cálculo \(\lambda\) de Alonzo Church. La \(\lambda\)-abstracción nos da una forma de escribir funciones. Por ejemplo, una expresión como \(f(x) = \Phi\), para \(\Phi\) una expresión que puede o no contener la variable \(x\), podemos reescribirla como \(\lambda x.\Phi\). Esta notación nos dice que estamos tomando la variable \(x\) y asignándola a la expresión \(\Phi\). Otra notación equivalente, y quizá más familiar al lector, es \(x \mapsto \Phi\). Así, la regla de introducción nos dice lo siguiente:

Es decir, que para especificar un término de \(A \rightarrow B\) debemos especificar un \(b:B\) para cada \(a:A\) tal que \(a \mapsto b\). La regla de eliminación precisamente nos muestra cómo aplicar la función dada una entrada:

En este caso no usamos \(\lambda\)-abstracción en tanto no especificamos qué valor obtiene \(f(a)\). Ahora, ya que la \(\lambda\)-abstracción nos da una función \(\lambda x.\Phi\), podemos aplicarla a una entrada \(y\) tal que \((\lambda x.\Phi)(y) \equiv \Phi\lbrack y/x\rbrack\). Esto nos dice la regla de computación:

Ahora iremos un poco más rápido, poniendo al lado de cada derivación qué regla se está aplicando y dando una breve explicación intuitiva de lo que significan al final. Empecemos por el tipo producto:

La regla de introducción afirma que los términos son pares ordenados \((a,b)\). La regla de eliminación nos afirma que, dado un término del tipo, tendremos dos funciones proyección \(\pi_{1},\pi_{2}\) que llevan cada componente del par ordenado a su respectivo tipo, hecho que se hace explícito con la regla de computación.

Un tipo análogo al tipo producto² es el tipo coproducto o tipo suma \(A + B\).

Los términos \(s:A + B\) tienen dos etiquetas, \(\iota_{1}(a)\) y \(\iota_{2}(b)\), representando términos de \(A\) y \(B\) respectivamente, como una suma de ambos términos. La regla de eliminación presupone que \(C\) es un tipo que nos dará una familia sobre \(A + B\); dada esa familia, podremos construir secciones de la fibra \(C(z)\) usando los elementos \(x,y\) de la suma \(z:A + B\), i.e. \(c(x)\) y \(d(y)\). Dado otro habitante \(t:A + B\), la regla de eliminación, la última escrita, nos dice que podremos construir una sección de la fibra \(C(t)\) usando las dos secciones de \(C(z)\) construidas anteriormente. Las dos reglas de computación, que no escribimos por brevedad, aplican la eliminación dados términos \(a:A,\ b:B\), tal que se construyen secciones para las fibras \(C\left( \iota_{1}(a) \right)\) y \(C\left( \iota_{2}(b) \right)\).

Veamos ahora el tipo de funciones dependientes.

Una función dependiente es una función cuyo codominio es un tipo dependiente del valor de entrada de la función. Así para formar el tipo de función dependiente necesitamos una familia \(B\) sobre \(A\). La introducción muestra que sus términos son funciones dependientes que envían cada entrada a una sección de la familia, hecho que tanto la eliminación como computación ejemplifican con una entrada \(a:A\). También se conoce a este tipo como tipo de producto dependiente, debido a que puede interpretarse como el producto cartesiano de una familia de conjuntos \(B(x)\) indexados por \(x:A\). Nótese que las funciones dependientes generalizan las funciones ordinarias. Ahora, dada la misma familia \(B\) sobre \(A\), podemos considerar pares ordenados \((a,b)\) donde \(b:B(a)\) depende de \(a:A\), generalizando el producto ordinario. Esto nos da el tipo de suma dependiente, también llamado tipo de par dependiente:

Finalmente, tendremos el tipo vacío \(\mathbb{0}\) y el tipo unidad \(\mathbb{1}\). Por brevedad, no nos centraremos en sus reglas, sino en dos propiedades importantes. El tipo unidad puede construirse en cualquier contexto, los cuales además derivan que tiene un solo habitante \(\mathbb{*:1}\). Una función \(\mathbb{1 \rightarrow}A\) a un tipo arbitrario \(A\) selecciona un término particular \(a:A\). El tipo vacío en cambio no tiene elementos, por lo que tampoco tiene regla de introducción ni de computación. Su regla de eliminación nos dice que si asumimos un habitante \(p\mathbb{:0}\) podremos construir un habitante para cualquier tipo \(C\) arbitrario. Esta extraña regla quizá recuerde al lector al principio de explosión de la lógica clásica, o que de una contradicción se sigue lo que sea. Efectivamente, ambas reglas corresponden bajo la correspondencia Curry-Howard, que exploramos ahora en la siguiente sección.

Curry-Howard, tipos identidad y universos

Según la correspondencia Curry-Howard, cada tipo puede interpretarse como una proposición y cada término como una demostración suya. Bajo esta interpretación, \(A \times B\) corresponde a la conjunción \(A \land B\), \(A + B\) corresponde a la disyunción \(A \vee B\), \(A \rightarrow B\) corresponde al condicional \(A \Rightarrow B\), \(B(x)\) corresponde a un predicado, \(\Pi_{x:A}B(x)\) corresponde a \(\forall xB(x)\), \(\Sigma_{x:A}B(x)\) corresponde a \(\exists xB(x)\) y \(\mathbb{1,\ 0}\) corresponden a verdadero \(\top\) y falso \(\bot\) respectivamente.

Ahora puede verse, por ejemplo, que la regla de eliminación de \(A \rightarrow B\) corresponde al modus ponens: si el condicional es cierto \(f:A \rightarrow B\) y \(a:A\) es cierta, entonces \(f(a):B\) es cierta. O la regla de introducción del coproducto con la regla de introducción de \(\vee\): si \(a:A\) es cierta la disyunción \(\iota_{1}(a):A + B\) es cierta, i.e. \(A \Rightarrow A \vee B\), y las proyecciones de \(A \times B \rightarrow ,A,\ B\) refleja que si \(A \land B\) entonces \(A\) y \(B\). El lector puede verificar que el resto de reglas de introducción y eliminación de cada tipo corresponden a las reglas de introducción y de eliminación de sus correspondientes contrapartes lógicas en deducción natural. De esta manera, MLTT puede realizar derivaciones lógicas dentro de su propia teoría, y no en una metateoría. Sin embargo, la lógica que MLTT incorpora bajo esta correspondencia no es la lógica clásica, sino la lógica intuicionista. En particular, esta correspondencia entre tipos y operadores lógicos mediante reglas de inferencia y demostraciones de proposiciones se inspira fuertemente en la interpretación constructivista Brouwer-Heyting-Kolmogorov (BHK) de los operadores lógicos.

Según Heyting, por ejemplo, una proposición expresa una intención, o expectativa, de una demostración de tal proposición. Similarmente, Kolmogorov entendía una proposición como expresando una tarea o problema a resolver. En ambos casos, la verdad de una proposición está determinada por la existencia de una demostración o una solución, i.e. depende de construir explícitamente una prueba lo que expresa; “la propiedad de ser verdad es la misma que la de ser demostrable […] la noción de una demostración de una proposición es conceptualmente previa a la noción de verdad” (Martin-Löf, 1987, p. 414, traducción mía). Dos hechos notables que trae consigo la lógica intuicionista de MLTT es que no se asume el principio de tercero excluido \(A \vee \neg A\) ni la doble negación \(\neg\neg A = A\), por lo que la prueba por contradicción tampoco es válida. Para ver esto, bajo la correspondencia Curry-Howard definiremos la negación como \(\neg A: = A\mathbb{\rightarrow 0}\), i.e. que \(A\) implica una contradicción \(\bot\). La prueba por contradicción se vuelve \((\neg A \rightarrow \bot) \rightarrow A\) que por la definición de negación se convierte en \(\neg\neg A \rightarrow A\), i.e., la regla de doble negación. El hecho de que \(\neg\neg A\) esté habitado implica que ninguna refutación de \(A\) es posible; pero esto no implica que \(A\) esté habitado. Constructivamente, \(\neg\neg A \rightarrow A\) será inválido. Del mismo modo, \(A \vee \neg A\) será inválido en tanto nada asegura que, en principio, podamos construir una demostración de \(A\) o de \(\neg A\). A pesar de esto, MLTT tampoco rechaza el tercero excluido y, en breve, veremos cómo poder recuperar la lógica clásica en MLTT.

Ahora, vimos que los tipos dependientes pueden verse como predicados sobre términos. Uno de los predicados que podemos formar es el predicado que afirma que dos términos \(a,b:A\) son proposicionalmente iguales, \(a =_{A}b\). El tipo que expresa esta proposición se llama tipo identidad, \(Id_{A}(a,b)\). Sus reglas de formación e introducción afirman:

La formación nos dice que podemos formar la proposición \(a =_{A}b\) para cualesquiera elementos \(a,b:A\), sea cierta o falsa. La introducción nos dice que, como mínimo, sabemos que la igualdad proposicional es reflexiva, por lo que \(a =_{A}a\) tendrá un habitante \(r_{A}(a)\). Nótese que gracias a la regla de introducción podemos probar que \(a \equiv b:A\) implica \(a =_{A}b\), usando reflexividad bien sea sobre \(a\) o \(b\). El recíproco, sin embargo, no es siempre válido. En el caso de la interpretación Curry-Howard, y otros modelos extensionales, de la igualdad proposicional podremos derivar una igualdad definicional, llamada la regla de reflexión. Como veremos en la sección 3, la novedad de la interpretación homotópica es que la igualdad proposicional es mucho más laxa, por lo que \(a =_{A}b\) no implica necesariamente \(a \equiv b\). Los modelos donde ocurre este hecho son intensionales.

Con esto en mente, podemos volver a una antigua distinción hecha por Frege (1892): el sentido y la referencia. La referencia de una palabra es a aquello que refiere o denota. Cuando apunto el dedo a la persona frente a mí y digo: “este hombre”, la persona frente a mí será su referente. El sentido de una palabra, en cambio, es la forma en que su referente es presentado. Si la persona frente a mí resulta ser Marlon Brando, entonces tanto “Marlon Brando” como “este hombre” le tendrán de referente. Sin embargo, es claro que cuando yo afirmo: “este hombre es Marlon Brando”, existe diferencia entre ambos términos, en tanto “este hombre es Marlon Brando” no informa necesariamente lo mismo que la tautología “este hombre es este hombre”. De esta forma, en modelos extensionales términos co-referenciales son iguales, pero en contextos intensionales no necesariamente. La co-referencia puede interpretarse como igualdad proposicional, mientras que la igualdad definicional funcionaría como dos términos compartiendo tanto referencia como sentido.

La regla de eliminación del tipo identidad, también llamada regla J, termina de caracterizar a la igualdad proposicional:

La regla J nos dice que si tenemos un predicado \(C\) que depende de pares de términos de \(x,y:A\) y de una prueba de su igualdad proposicional \(p:Id_{A}(x,y)\), entonces si el predicado \(C\) es cierto para la identidad trivial reflexiva de \(x\), \(r_{A}(x):x =_{A}x\), podremos construir una demostración de su verdad para la identidad \(p:Id_{A}(x,y)\) transportando la demostración \(t(x):C\left( x,x,r_{A}(x) \right)\) sobre la identidad entre \(x\) y \(y\). En resumen, si un predicado es cierto para la identidad trivial \(x =_{A}x\), también será cierto para cualquier otra identidad con \(x\), \(x =_{A}y\). Con esta regla es posible demostrar que la igualdad proposicional es una relación de equivalencia y satisface reglas de sustitución similares, aunque un poco más débiles, que aquellas de la identidad definicional.

Ahora, según la correspondencia Curry-Howard absolutamente todo tipo puede interpretarse como una proposición. Sin embargo, muchos tipos no parecen comportarse como proposiciones tradicionales. Por ejemplo, tipos con múltiples términos son proposiciones con múltiples formas de ser verdad. Para remediar estos problemas, definiremos como proposiciones genuinas, o meras proposiciones, aquellos tipos vacíos o con un único término. Así, un tipo \(A\) será una mera proposición si el tipo \(\Pi_{x:A}\Pi_{y:A}\ x =_{A}y\) está habitado. De hecho, podemos convertir a todo tipo en una proposición “olvidando” la información de sus habitantes más allá de su mera existencia, bajo un proceso llamado truncación proposicional o \(( – 1)\)-truncación. Para todo tipo \(A\), su \(( – 1)\)-truncación será el tipo \(||A||\), tal que para todo \(a:A\) tendremos \(||a||:||A||\) y para cualesquiera \(x,y:||A||\) tendremos \(x =_{||A||}y\).

Hemos visto ya, por ejemplo en la definición de mera proposición, la aplicación del tipo \(\Pi_{x:A}\) como un cuantificador universal. ¿Pero qué ocurre si queremos cuantificar sobre tipos? ¿O qué ocurre si queremos hablar de identidad entre tipos? El problema en ambos casos es que estos conceptos sólo están definidos para términos. Parece que la solución más sencilla de implementar es poder convertir a todo tipo en término de algún otro tipo. Una primera intuición podría ser introducir un tipo \(\text{Type}\) tal que si \(\Gamma \vdash A\ \text{type}\) entonces \(\Gamma \vdash A:\text{Type}\). Sin embargo, asumir este tipo de todos los tipos, que nos lleva al juicio \(\text{Type}:\text{Type}\), deriva una contradicción, hecho descubierto por Girard (1972) como análogo a la paradoja de Russell para la teoría de conjuntos naive. Lo que haremos será entonces postular una jerarquía cumulativa de universos, conocidos como universos de Russell, \(\mathcal{U}_{1}:\mathcal{U}_{2}:\ \ldots\ \mathcal{U}_{i}:\mathcal{U}_{i + 1}:\ \ldots\), con las siguientes reglas:

Ahora podemos hablar, por ejemplo, de la igualdad proposicional entre tipos \(A =_{\mathcal{U}_{i}}B\). A la vez, la definición de los tipos dependientes se simplifica un poco más: podemos ver una familia \(B\) sobre \(A\) como un término del tipo \(A \rightarrow \mathcal{U}_{i}\), pues a cada \(x:A\) se le asigna un tipo \(B(x)\). Finalmente, también podemos cuantificar sobre tipos. Por ejemplo, si \(\mathcal{U}_{- 1}\) es el universo de meras proposiciones (o tipos \(( – 1)\)-truncados), entonces podemos definir el tercer excluido como la proposición \(\Pi_{A:\mathcal{U}_{- 1}}A + \neg A\). Como mencionamos anteriormente, en tanto MLTT no rechaza el tercer excluido, podemos agregar esta proposición como axioma. De hecho, el tercer excluido y la doble negación son equivalentes en la propia lógica intuicionista, lo que significa que asumiendo cualquiera como axioma puede derivarse la otra. De esta manera, agregando \(\Pi_{A:\mathcal{U}_{- 1}}A + \neg A\) a MLTT podemos recuperar la lógica clásica.

Pero, ¿qué pasa si agregamos estas reglas clásicas para tipos arbitrarios? Si bien el tercer excluido para tipos arbitrarios, y por tanto la doble negación, no es inconsistente con MLTT, sí que cambia profundamente su comportamiento. Se pierden propiedades computacionales como la canonicidad y la interpretación constructivista BHK queda descartada. Más importante, se pierde la riqueza del tipo identidad. Usando este tercer excluido sin restricciones, es posible derivar el principio de unicidad de pruebas de identidad (UIP, en inglés), según el cual cualesquiera dos pruebas de la identidad de dos términos \(p,q:a =_{A}b\) son también iguales proposicionalmente, i.e.

(UIP) \(\ \Pi_{a:A}\Pi_{b:A}\Pi_{p:Id_{A}(a,b)}\Pi_{q:Id_{A}(a,b)}\ Id_{Id(a,b)}(p,q)\).

Esto implica que para cualquier tipo y cualesquiera de sus términos, el tipo identidad será una mera proposición, quitando así parte de la riqueza del tipo identidad que la interpretación homotópica explota. Asumiendo el tercer excluido irrestricto, y por tanto el UIP, no sólo retomamos la lógica clásica sino que quitamos parte del carácter computacional, constructivista y homotópico que MLTT permite. Así, únicamente consideraremos sus versiones para tipos \(( – 1)\)-truncados a la hora de trabajar lógica clásica en MLTT.

Teoría Homotópica de Tipos

Caminos y homotopía

La noción de espacio topológico pretende capturar la idea de un espacio, compuesto por puntos que se conectan entre sí de forma continua. En su definición conjuntista, un espacio topológico \(\langle X,\tau\rangle\) consiste en un conjunto \(X\) y una colección \(\tau\) de subconjuntos de \(X\) que pueden considerarse como vecindarios que contienen puntos, y que satisfacen ciertos axiomas. Los elementos \(x \in X\) pueden considerarse puntos del espacio. Dados dos puntos \(a,b \in X\), un camino entre ellos es una función continua \(\eta:\lbrack 0,1\rbrack \rightarrow X\) del intervalo cerrado entre 0 y 1 al espacio, tal que \(\eta(0) = a\) y \(\eta(1) = b\). Una función continua \(f\), intuitivamente, es una función tal que sus valores de salida no tienen “grandes saltos”, i.e. si dos valores de entrada se aproximan \(x_{1} \approx x_{2}\) entonces también sus valores de salida \(f\left( x_{1} \right) \approx f\left( x_{2} \right)\).³ Un camino, de esta forma, nos da una trayectoria continua entre \(a\) y \(b\) parametrizada por el intervalo \(\lbrack 1,0\rbrack.\) También puede interpretarse como una deformación continua entre dos puntos. Así, además de deformaciones continuas entre puntos también tendremos deformaciones continuas entre esas mismas deformaciones continuas, concepto capturado por la noción de homotopía. Dos funciones \(f,g:X \rightarrow Y\) son homotópicas, denotado por \(f \sim g\), si existe una función continua \(\phi:\lbrack 0,1\rbrack \times X \rightarrow Y\) tal que \(\phi(0,x) = f(x)\) y \(\phi(1,x) = g(x)\) para todo \(x \in X\). Algo importante de notar es que los caminos son casos especiales de homotopías (entre funciones constantes).

Según la interpretación homotópica de MLTT, iniciada y desarrollada por Hoffman & Streicher (1994), Awodey & Warren (2009) y Lumsdaine, Kapulkin & Voevodsky (2012), interpretaremos los tipos como espacios topológicos y sus términos como puntos del espacio. Bajo esta interpretación, el tipo producto es el espacio producto de dos espacios, el tipo coproducto es la unión disjunta de espacios y el tipo función es el espacio de funciones entre dos espacios. El tipo \(\mathbb{1}\) es el espacio \(\mathbf{1}\) con un único punto, y el tipo \(\mathbb{0}\) es simplemente el conjunto vacío \(\varnothing\), el cual también es un espacio topológico. Para entender los tipos dependientes necesitaremos primero la noción de fibración.

En una fibración tendremos un espacio base \(B\), un espacio total E y una función continua \(p:E \rightarrow B\). Si \(b \in B\), llamamos fibra a la preimagen \(p^{- 1}(b)\). Una fibración, intuitivamente, puede entenderse como una familia de espacios \(E\) parametrizada continuamente por una base \(B\). Pensemos por ejemplo en un cilindro. Un cilindro, en resumen, es un círculo (por ejemplo en el plano \(XY\)) que se extiende sobre otro eje (por ejemplo el eje \(Z\)), que nos dará su altura; así podríamos representarlo como \(\mathbb{S}^{1} \times \lbrack 0,1\rbrack\) (o cualquier otro intervalo), donde \(\mathbb{S}^{1}\) es el círculo unitario y el producto con un intervalo nos da la altura del cilindro. Este cilindro será nuestro espacio total, y el círculo unitario el espacio base. Así nuestra fibración \(p:\mathbb{S}^{1} \times \lbrack 0,1\rbrack \rightarrow \mathbb{S}^{1}\) será dada por \(p(\theta,t) = \theta\). Como trabajamos en un círculo, i.e. todos los puntos cuya distancia, o norma, al centro es constante, todo punto estará definido por el ángulo \(\theta\) que abre con respecto a un eje de referencia. Como es un cilindro, también podremos pensar en la altura \(t\) de ese punto. Nuestra fibración, que como vemos se asemeja también a las proyecciones del producto, olvida la altura del punto y sólo considera su ángulo. Esto es como proyectar, o aplanar, un punto del cilindro en el plano donde está el círculo. Si ahora tomamos un punto \(b \in \mathbb{S}^{1}\) y vemos su imagen inversa \(p^{- 1}(b)\), esta imagen inversa será una línea recta que nace del punto \(b\) en el círculo y se extiende por toda la altura del intervalo, como una especie de cabello o fibra que emerge de \(b\). Espero que la explicación anterior ilustre un poco más las interpretaciones del resto de tipos: los tipos dependientes \(B(x)\) serán fibraciones, un \(b(x):B(x)\) será una sección de la fibración, \(\Pi_{x:A}B(x)\) es el espacio de todas las secciones y \(\Sigma_{x:a}B(x)\) es el espacio total.

Finalmente, el tipo identidad \(a =_{A}b\) se interpreta como un camino entre dos puntos. Aquí es precisamente donde la estructura enriquecida de la identidad surge. Supongamos que dados dos términos \(a,b:A\) tenemos la siguiente cadena de igualdades proposicionales:

\[p,q:Id_{A}(a,b)\ ;\ \alpha,\beta:Id_{Id_{A}(a,b)}(p,q)\ ;\ \lambda,\mu:Id_{Id_{Id_{A}(a,b)}(p,q)}(\alpha,\beta)\ ;\ldots\]

Si esta cadena continúa al infinito, tendremos la estructura de un \(\infty\)-grupoide. En su sentido más general, un \(\infty\)-grupoide es una \((\infty,0)\)-categoría, i.e., una \(\infty\)-categoría donde todo \(k\)-morfismo es una equivalencia, o invertible.⁴ Intuitivamente, esto significa que tendremos una colección de objetos con morfismos, o funciones, entre ellos, 2-morfismos entre los morfismos, 3-morfismos entre los 2-morfismos… ad infinitum. En nuestro caso particular, los objetos son el par de términos \(a,b:A\), los 1-morfismos entre ellos son los caminos \(p,q:Id_{A}(a,b)\), los 2-morfismos son las homotopías \(\alpha,\beta\) entre los caminos, los 3-morfismos son las homotopías \(\mu,\lambda\) entre las homotopías \(\alpha,\beta\), y así sucesivamente. En tanto la relación de homotopía, y por tanto la relación de tener un camino, es una relación de equivalencia, cada uno de estos \(k\)-morfismos son invertibles y por tanto equivalencias.

Cabe notar que esta estructura de \(\infty\)-grupoide del tipo identidad es una estructura potencial, i.e., no todo tipo cumple que sus tipos identidad de mayor orden forman un \(\infty\)-grupoide. Si nos centramos en tipos con menor estructura homotópica entonces nos centramos en tipos que colapsan ciertas igualdades proposicionales. Vimos ya, por ejemplo, que las proposiciones son tipos \(( – 1)\)-truncados donde todos los términos colapsan, i.e., el tipo o está inhabitado o tiene un único habitante. En el siguiente nivel, la 0-truncación, podremos tener múltiples términos distintos en un tipo, sin embargo, todos los tipos identidad de esos términos son proposiciones. Esto quiere decir que aunque los términos no colapsan, sus identidades sí. Los tipos 0-truncados se definen como conjuntos. Nótese aquí que no estamos hablando de la interpretación conjuntista de MLTT mencionada anteriormente, la cual sólo puede realizarse en una versión extensional de MLTT que HoTT precisamente descarta. En cambio, dentro de HoTT estamos definiendo tanto la noción de proposición como la noción de conjunto mediante truncaciones. Otra observación importante es la relación entre tipos 0-truncados y el UIP. Recordemos que el UIP afirma que cualesquiera dos pruebas de identidad son idénticas, que es precisamente lo que ocurre en la 0-truncación. Así, otra manera de interpretar el UIP es la imposición de que todos los tipos son conjuntos. El resto de truncaciones no las veremos aquí, aunque su definición recursiva es sencilla: un tipo es \((k + 1)\)-truncado si el tipo identidad de todos sus términos es \(k\)-truncado.

Ahora con conjuntos incorporados en HoTT, podremos definir también las categorías, subsumiendo así los otros dos marcos fundacionales principales de las matemáticas. La categoría de conjuntos \(Set\) en HoTT cumplirá también algunas propiedades de la categoría de conjuntos en la teoría de categorías estándar, aunque para que ambas categorías correspondan necesitamos un axioma adicional particular: el redimensionamiento proposicional, según el cual toda proposición en un universo \(\mathcal{U}_{i + 1}\) puede ser redimensionada a una proposición equivalente en el universo más pequeño \(\mathcal{U}_{i}\). Añadir este axioma implica que la categoría \(Set\) tiene un clasificador de subobjetos y es por tanto un topos elemental. Uno puede añadir el axioma de elección y el tercer excluido, i.e. asumir que son ciertas con sus cuantificadores restringidos a conjuntos y proposiciones respectivamente, para recuperar la teoría clásica de conjuntos. Esto le permite a HoTT fundamentar todas las matemáticas vía las fundamentaciones que hacen la teoría de conjuntos y la teoría de categorías. De hecho, en algunos aspectos HoTT parece funcionar como un fundamento más natural, en tanto facilita parte de la filosofía estructuralista de la teoría de categorías, y permite una aproximación más directa a la teoría de \(\infty\)-categorías, difícil de concretar usando conjuntos.

Sin embargo, para poder discutir estas ideas con más precisión, necesitaremos antes el axioma de Univalencia, el cual discutiremos en la sección 3.3. Antes de pasar a este axioma, vale la pena visitar otras cualidades interesantes del tipo identidad. En particular, nos centraremos ahora en la forma en que HoTT valida la regla de J del tipo identidad.

Inducción de caminos

Recordemos que la regla J nos da un esquema tal que si un predicado \(C\) es cierto para \(x:A\) y su identidad reflexiva \(x =_{A}x\), entonces es cierto también para cualquier igualdad proposicional \(x =_{A}y\) con \(x\). En las interpretaciones extensionales de MLTT, la regla J se vuelve prácticamente trivial. Si \(p:Id_{A}(x,y)\) entonces \(x \equiv y\), por lo que \(C\left( x,x,r_{A}(x) \right) \equiv C(x,y,p)\) por definición. En las teorías intensionales, y sobre todo aquellas donde el UIP no se sostiene, la regla J adquiere un carácter más interesante.

Si traducimos la regla J bajo la interpretación homotópica, entonces esta afirmará que dado un predicado \(C\) que toma puntos \(a,b:A\) y caminos entre ellos, si \(C\) es cierta para el camino trivial \(r_{A}(x):x =_{A}x\) entonces es cierta para todo camino en el espacio \(A\). Esta interpretación se conoce como inducción de caminos. La inducción en matemáticas es un esquema que nos permite inferir que una cierta propiedad se da para una clase entera de objetos. El ejemplo más clásico es la inducción sobre los números naturales, el cual es un axioma de la aritmética de Peano. La inducción aritmética tiene dos partes: primero, probamos que la propiedad se cumple para el 0 o para el 1, llamado caso base; después se prueba que, suponiendo que la propiedad se cumple para \(n\), la hipótesis de inducción, entonces se cumple para \(n + 1\). Si estas dos cosas se cumplen, la propiedad se cumple para todo número natural. Intuitivamente, la inducción es una regla válida ya que nos da un esquema para, en principio, demostrar caso a caso que la propiedad se cumple. Empezamos con el caso base 0, y después ya sabemos cómo proceder para demostrar que se cumple para \(n + 1\) dado que se cumple para \(n\), por lo que ya sabemos cómo demostrarlo para 1, 2, 3, …, etc. La inducción de caminos nos da algo similar, aunque sin hipótesis inductiva. Aquí sólo necesitaremos que se cumpla el caso base, el camino trivial, y después podremos inferir que se cumple para todo camino en ese punto.

Fuera de aplicaciones en teoría de homotopía y topología algebraica, quizá la aplicación más importante de la inducción de caminos, y la regla J en general, es probar la regla de transporte:

\(\Pi_{A:\mathcal{U}_{i}}\ \Pi_{P:A \rightarrow \mathcal{U}_{i}}\ \Pi_{x\ y:A}\ \left( x =_{A}y \right) \rightarrow P(x) \rightarrow P(y)\).

Esta regla dice que dada una familia \(P\) sobre \(A\), o un predicado \(P\), y \(x =_{A}y\), entonces si el predicado es cierto para \(x\) también lo es para \(y\). Esta regla es una forma de la ley de Leibniz, o el principio de indiscernibilidad de los idénticos. Esta relación con uno de los principios más conocidos, y controversiales, de la identidad la exploraremos en la segunda parte.

Por ahora, visitaremos el axioma de Univalencia, quizá la característica más novedosa de HoTT.

El axioma de Univalencia

La Univalencia es una propiedad que pueden exhibir los tipos identidad en un cierto universo. Gracias a la interpretación homotópica de HoTT, podemos heredar de la teoría de homotopía clásica las nociones de fibras homotópicas y de equivalencias homotópicas entre espacios topológicos. El axioma de Univalencia nos afirma, resumidamente, que la equivalencia homotópica entre tipos y la igualdad proposicional entre tipos \(Id_{\mathcal{U}_{i}}(A,B)\) corresponden. En forma de slogan: la equivalencia es equivalente a la identidad. Precisar estas ideas nos tomará algunos pasos un poco técnicos.

Primero, un tipo es contraíble si todos sus términos son idénticos a un único elemento, i.e. si todos sus puntos pueden contraerse en un único punto mediante caminos

\(isContr(A): = \Sigma_{a:A}\Pi_{b:A}\left( a =_{A}b \right)\).

Dados \(f:A \rightarrow B\), \(y:B\), la fibra de \(f\) sobre \(y\) se define como

\(f^{- 1}(y): = \Sigma_{x:A}\ Id_{B}\left( f(x),y \right)\).

Esta definición de fibra es similar a la noción de fibra vista anteriormente: es la preimagen de un punto \(y:B\) bajo \(f\). Esto quiere decir que la fibra son todos los puntos \(x:A\) que son enviados a \(y:B\) bajo \(f\), i.e. todas las \(x:A\) tales que \(f(x) =_{B}y\). Con estos dos conceptos, podemos definir que una función \(f\) es una equivalencia cuando todas sus fibras son contraíbles

\(isEquiv(f): = \Pi_{y:B}\ isContr\left( f^{- 1}(y) \right)\).

Intuitivamente, si las fibras son contraíbles entonces para todo \(y:B\) existe un único \(x:A\) tal que \(f(x) =_{B}y\), por lo que la función es de cierta forma una biyección. Esto quiere decir que \(A\) y \(B\) tienen la misma cantidad de términos (al menos hasta igualdad proposicional) y que existe una correspondencia uno a uno entre ellos, i.e. a todo elemento de \(A\) le corresponde un único elemento de \(B\) y viceversa. Hay, de hecho, múltiples definiciones equivalentes de equivalencia (véase The Univalent Foundations Program 2013, Cap. 4). Nosotros sólo nos centraremos en otra definición para ilustrar mejor el concepto.

Decimos que entre dos funciones \(f,f’:A \rightarrow B\) existe una homotopía \(f \sim f’\) cuando el tipo \(\Pi_{x:A}\ f(x) = f'(x)\) está habitado. Esto quiere decir que las dos funciones devuelven valores iguales con entradas iguales. El lector acostumbrado a la teoría de conjuntos recordará que esta definición clásicamente implica que \(f\) y \(f’\) son iguales como funciones, lo que se conoce como extensionalidad de funciones. En HoTT podremos recuperar la extensionalidad de funciones bien sea agregándola como principio, o derivándola del axioma de Univalencia. Asumiendo entonces la extensionalidad de funciones, identificaremos \(f \sim f’\) con \(f = f’\). Nuestra segunda definición de equivalencia nos dice

\(isEquiv(f): = \left( \Sigma_{g:B \rightarrow A}\ f \circ g = 1_{B} \right) \times \left( \Sigma_{h:B \rightarrow A}\ h \circ f = 1_{A} \right)\).

Donde \(\circ\) es la composición de funciones y \(1_{B}\), \(1_{A}\) son las funciones identidad sobre \(B\) y \(A\), respectivamente, que para toda entrada \(x\) devuelven la misma \(x\). Esta definición entonces quiere decir que existen dos funciones \(g,h:B \rightarrow A\) tales que si primero aplico \(g:B \rightarrow A\) a una entrada \(y:B\) y luego \(f:A \rightarrow B\) a la entrada \(g(y)\) entonces \(f\left( g(y) \right) = y\), i.e. volveremos a un punto igual a nuestro punto de partida. De igual forma si primero aplico \(f:A \rightarrow B\) a una entrada \(x:A\) y luego \(h:B \rightarrow A\) a la entrada \(f(x)\) entonces \(h\left( f(x) \right) = x\). Ahora, esta igualdad no es estricta, más bien los puntos \(f\left( g(y) \right)\) y \(h\left( f(x) \right)\) tienen caminos a los puntos \(y,\ x\). Podemos ilustrar la situación de la siguiente forma:

Figura 1: Una equivalencia entre tipos.

Por supuesto, este camino entre \(x\) y \(h\left( f(x) \right)\) implica en HoTT su igualdad. Así, de la misma manera que en la primera definición, para todo término en \(x:A\) existe un único término en \(y:B\) que le corresponde, y viceversa, donde aquí único significa que si \(y_{1}\) y \(y_{2}\) corresponden a \(x\), entonces hay un camino entre entre ellos, como ilustra la figura 1.

Con ambas definiciones de equivalencia a la mano, que podemos usar intercambiablemente, definimos el tipo equivalencia entre dos tipos \(A,B\), que simplemente afirma que existe una equivalencia entre ambos.

\(Eq(A,B): = \Sigma_{f:A \rightarrow B}\ isEquiv(f)\).

Si este tipo está habitado, i.e., si \(A\) y \(B\) tienen una equivalencia, entonces son tipos equivalentes, lo que denotamos por \(A \simeq B\).

Ahora, usando inducción de caminos y le regla de transporte definida en la sección anterior, construiremos la función

\(idtoeq:\left( A =_{\mathcal{U}_{i}}B \right) \rightarrow (A \simeq B)\).

Sea \(p:A =_{\mathcal{U}_{i}}B\), el transporte nos dice que dada una fibración, o familia de tipos, o predicado, \(P\) tendremos \(P(A) \rightarrow P(B)\). Definiremos \(P\) como \(1_{\mathcal{U}_{i}}\), la identidad sobre el universo que para todo \(X:\mathcal{U}_{i}\) devuelve el mismo \(X\). Entonces el transporte \(p*\) de \(p\) nos dará la función \(A \rightarrow B\). Nosotros queremos probar que \(isEquiv(p*)\). Sea \(Q(A,B,p): = isEquiv(p*)\), ahora podemos aplicar inducción de caminos sobre \(Q\) ya que toma como argumentos términos de un tipo e identidades entre ellos. Según la inducción, basta demostrar el caso \(Q\left( A,A,r_{\mathcal{U}_{i}}(A) \right)\), lo cual es claramente cierto en tanto si \(p\) es \(r_{\mathcal{U}_{i}}(A)\), i.e. la identidad trivial entre \(A\), entonces \(p*\) es \(1_{A}:A \rightarrow A\), la función identidad sobre \(A\), que es una equivalencia, como puede verse usando cualquiera de las dos definiciones. De esta forma, gracias a la inducción de caminos tendremos que \(isEquiv(p*)\), lo cual nos da \(A \simeq B\).

MLTT, por tanto, es capaz de demostrar, usando la regla J, que la identidad entre tipos implica su equivalencia. Lo que el axioma de Univalencia agrega es que la función idtoeq sea una equivalencia, hecho que MLTT no puede demostrar por su cuenta.

Axioma de Univalencia. Para cualesquiera \(A,B:\mathcal{U}_{i}\), idtoeq es una equivalencia, i.e.

\(\text{ua: }\left( A =_{\mathcal{U}_{i}}B \right) \simeq (A \simeq B)\).

Para nuestros propósitos posteriores en la siguiente parte de esta bilogía, será conveniente pensar el axioma de Univalencia como compuesto de dos partes: la primera afirma que existe una función \(eqtoid:A \simeq B \rightarrow A =_{\mathcal{U}_{i}}B\), conocida como Univalencia débil, mientras que la segunda afirma que \(eqtoid\) (o, equivalentemente, \(iqtoed\), ya que la equivalencia es una relación simétrica) es una equivalencia. En la siguiente parte precisamente exploraremos un poco más la Univalencia débil y su relación con el estructuralismo matemático. Por otra parte, la Univalencia es, estrictamente, una propiedad que cumple un universo particular, por lo que si \(isUniv\left( \mathcal{U}_{i} \right): = \Pi_{A,B:\mathcal{U}_{i}}\ isEquiv(idtoeq)\) está habitado, es decir si \(\mathcal{U}_{i}\) satisface el axioma de Univalencia, entonces decimos que \(\mathcal{U}_{i}\) es un universo Univalente. Por lo general, sin embargo, se asume que todos los universos son Univalentes cuando el axioma es adoptado.

El axioma de Univalencia, como mencionamos en la sección 3.1, permite un tratamiento algo más natural de la teoría de categorías. Por un lado, la teoría de categorías de mayor orden, i.e. la teoría de \(\infty\)-categorías, incorpora la noción de \(k\)-morfismos invertibles capturada también por el concepto de \(\infty\)-grupoide. Uno generalmente define una categoría (pequeña) como una clase de objetos con un conjunto de morfismos para cada par de objetos. Si en cambio permitimos que una categoría consista en un tipo de objetos y un tipo de morfismos, con toda la potencial estructura homotópica de ambos, podemos recuperar de forma más natural y directa la noción de \(\infty\)-categoría.

Por otro lado, y quizá más importante, es que HoTT podría también capturar de mejor forma la filosofía misma de las categorías. En la teoría de categorías un isomorfismo entre dos objetos de una categoría, \(X\) y \(Y\), se define como un par de funciones \(f:X \rightarrow Y,\ g:Y \rightarrow X\) tales que \(f \circ g = 1_{Y}\) y \(g \circ f = 1_{X}\), de manera análoga a la segunda definición de equivalencia vista anteriormente. Ahora, sin embargo, la composición de ambas funciones sí nos regresa al mismo punto de partida (véase la figura 2).

Figura 2. Un isomorfismo entre dos objetos de una categoría.

En los casos de isomorfismo tendremos una correspondencia uno a uno entre cada elemento que además preserva estructura. Así, cuando dos objetos en una categoría son isomorfos, tienen la misma estructura, y por tanto se los identifica como si fueran un único objeto. Esta práctica de identificar objetos isomorfos, común en la práctica matemática, no tiene una contraparte estrictamente formal, en tanto la teoría usada de base para fundamentar la teoría de categorías, generalmente la teoría de conjuntos o teoría de clases, identifica objetos de forma distinta y más estricta. Según ciertos autores (Awodey 2014, Chen 2024) el axioma de Univalencia puede interpretarse como la formalización de esta práctica, si uno interpreta, como parece natural según su segunda definición, la equivalencia de tipos como un isomorfismo. Pero es claro que la noción de equivalencia y la noción de isomorfismo, aunque muy similares, no son iguales. Sin embargo, estos problemas mas filosóficos quedarán para explorarse en la segunda parte.

Por supuesto, no hemos agotado en absoluto todo lo que HoTT ofrece a las matemáticas. Otra de sus innovaciones más notables son los tipos inductivos mayores (higher inductive types), que son una generalización de los tipos inductivos, los cuales son tipos construidos a partir de varios constructores de la forma

\[\mathcal{C}_{\mathcal{i}}:\mathcal{B}_{1} \rightarrow \mathcal{B}_{2} \rightarrow \ \ldots\ \rightarrow \ A\]

donde \(A\) es el tipo inductivo. Un ejemplo es el tipo de los naturales, definido a partir de una constante \(0\mathbb{:N}\) y una función sucesor \(\text{succ}\mathbb{:N \rightarrow N}\), a partir de la cual se construye el resto de términos. Los tipos inductivos de mayor orden no sólo construyen términos del tipo inductivo sino también términos de los tipos identidad entre términos, y potencialmente términos de las identidades entre identidades, etc. Sin embargo, estos tipos no tienen mucho interés filosófico, por lo que sólo los mencionamos de paso.

A pesar de estas y otra omisiones, esta introducción debería ser suficiente para que el lector pueda explorar por su cuenta desarrollos más avanzados en The Univalent Foundations Program (2013) o Rijke (2025), y que pueda introducirse a la discusión, a ser desarrollada en la siguiente ocasión, de las implicaciones y aplicaciones filosóficas de la teoría homotópica de tipos.

Agradecimientos

El autor quisiera agradecer a Martín Barra-Acuña y a Gabriel Donoso Umaña por motivar la escritura de esta bilogía de artículos, y a Omar Antolín Camarena y Navani Bautista por sus útiles comentarios y conversaciones.

REFERENCIAS

Altenkirch, T., Capriotti, P., Dijkstra, G., Kraus, N., & Nordvall Fors-berg, F. (2018). Quotient Inductive-Inductive Types. En Founda-tions of Software Science and Computation Structures (pp. 293-310). Springer International Publishing. https://doi.org/10.1007/978-3-319-89366-2_16

Antolín Camarena, O. (2016). A whirlwind tour of the world of (∞, 1)-categories [de Contemporary Mathematics, American Mathe-matical Society]. Mexican mathematicians abroad: recent contri-butions, ł57, 15-61. https://doi.org/10.1090/conm/657/13088

Awodey, S. (1996). Structure in mathematics and logic: A categorical perspective. Philosophia Mathematica, 4(3), 209-237. https://doi. org/10.1093/philmat/4.3.209

Awodey, S. (2014). Structuralism, Invariance, and Univalence. Philo-sophia Mathematica, 22(1), 1-11. https://doi.org/10.1093/ phimat/nkt030

Awodey, S., & Warren, M. (2009). Homotopy Theoretic Models of Identity Types. Mathematical Proceedings of the Cambridge Phi-losophical Society, 14ł(1), 45-55. https://doi.org/10.1017/ s0305004108001783

Chen, L. (2024). Univalence and Ontic Structuralism. Foundations of Physics, 54(3), 1-27. https://doi.org/10.1007/s10701-024-00768-4

Frege, G. (1892). Über Sinn Und Bedeutung. Zeitschrift für Philosophie Und Philosophische ffritik, 100(1), 25-50.

Girard, J.-Y. (1972). Interprétation Functionelle et fflimination Des Coupures Dans l’arithmétique d’ordre Supérieure. Tesis de Doc-torado.

Hofmann, M., & Streicher, T. (1994). The groupoid model refutes uniqueness of identity proofs. Proceedings Ninth Annual Iffffff Symposium on Logic in Computer Science, 208-212. https://doi. org/10.1109/lics.1994.316071

Ladyman, J., & Presnell, S. (2016). Does Homotopy Type Theory Provi-de a Foundation for Mathematics? The British Journal for the Phi-losophy of Science, ł9(2). https://doi.org/10.1093/bjps/axw006 Ladyman, J., & Presnell, S. (2020). The Hole Argument in Homotopy Type Theory. Foundations of Physics, 50(4), 319-329. https://doi.

org/10.1007/s10701-019-00293-9

Lumsdaine, P., Kapulkin, C., & Voevodsky, V. (2012). The simplicial model of univalent foundations [Preprint de arXiv]. http://arxiv. org/abs/1203.2553

Martin-Löf, P. (1975). An Intuitionistic Theory of Types. En P. Part (Ed.), Logic Colloquium 73 Proceedings of the Logic Colloquium (pp. 73-118). Elsevier.

Martin-Löf, P. (1987). Truth of a Proposition, Evidence of a Judgement, Validity of a Proof. Synthese, 73(3), 407-420. https://doi.org/10. 1007/bf00484985

Martin-Löf, P. (1998, octubre). An intuitionistic theory of types. En Twenty Five Years of Constructive Type Theory. Oxford University Press. https://doi.org/10.1093/oso/9780198501275.003. 0010

Rijke, E. (2025). Introduction to Homotopy Type Theory. Cambridge University Press. https://doi.org/10.1017/9781108933568

Rodin, A. (2024). Does Identity Make Sense? Manuscrito, 47(1), 2024-0073. https://doi.org/10.1590/0100-6045.2024.v47n1.ar

The Univalent Foundations Program. (2013). Homotopy Type Theory: Univalent Foundations of Mathematics [Institute for Advanced Study.]. https://homotopytypetheory.org/book

Tsementzis, D. (2017). Univalent Foundations as Structuralist Founda-tions. Synthese, 194(9), 3583-3617. https://doi.org/10.1007/ s11229-016-1109-x

Tsementzis, D. (2020). A meaning explanation for HoTT. Synthese, 197(2), 651-680. https://doi.org/10.1007/s11229-018-02052-1

NOTAS

Constantino Contreras es estudiante de la licenciatura en matemáticas en Universidad Autónoma de México y becario de su Instituto de Matemáticas. Email: mailto:constantino.contreras@ciencias.unam.mx. ORCID: https://orcid.org/0009-0000-2863-3465

Esto no quita que, si uno usa como metateoría otra teoría de tipos, entonces los juicios sí que pueden definirse como tipos usando tipos inductivos-cocientes inductivos (quotient inductive-inductive types; véase Altenkirch et al. (2018).

De hecho, en la interpretación categórica de la teoría de tipos (como una categoría cartesiana cerrada) el coproducto es el dual del producto.

Formalmente, \(f:X \rightarrow Y\) es continua si la preimagen de conjuntos abiertos en \(Y\) bajo \(f\) es también abierta.

El lector interesado puede consultar Antolín-Camarena (2016) para una introducción a las \(\infty\)-categorías.