Teoria homotópica de tipos

Archiu:Hott book cover.png

Portada de Homotopy Type Theory: Univalent Foundations of Mathematics.

En llògica matemàtica i ciències de la computació, la teoria homotópica de tipos (HoTT /hɒt/, per les seues sigles en anglés) són vàries llínees de desenroll de la Teoria de Tipos Depenents, basada en interpretar els tipos com a objectes als quals s'apliquen les intuïcions de la teoria de homotopía abstracta.

Açò inclou, entre atres llínees de treball, la construcció de models homotópicos usant les categories de models de Quillen per a teories de tipos categòriques (o categories cartesianas tancades); l'us de la teoria de tipos com a llògica (o llenguage intern) de la teoria de homotopía abstracta i teoria de categories d'orde superior; el desenroll de les matemàtiques dins de fonaments basats en teoria de tipos (incloent tant matemàtica existent com la matemàtica nova que els tipos homotópicos fan possible); i la formalisació de cada una d'estes llínees en assistents de demostració.

Introducció

Intuitivamente, la teoria homotópica de tipos (HoTT) interpreta la teoria de tipos de Martin-Löf de forma tal que cada tipo és un espai topològic i cada terme d'un tipo és un punt en tal espai. Formalment, Awodey i Warren introduïxen per primera volta el model homotópico utilisant les categories de models de Quillen, demostrant que estes categories, aixina com les categories simpliciales o les categories d'espais topològics, tenen una teoria de tipos de Martin-Löf com a llenguage intern.

HoTT estén la teoria de tipos de Martin-Löf usant conceptes de teoria homotópica i afegint axioma poc comuns com l'axioma de Univalencia. Ademés, el concepte d'identitat es relaixa totalment, en tant l'identitat entre térmens d'un tipo $x{=}_{A}y$ s'entén com un camí entre punts d'un espai $x,y:A$.

Per a parlar d'identitat de tipos, poden agregar-se univers a la teoria de tipos de Martin-Löf. La forma més usual és la jerarquia de Russell. Tindrem una jerarquia de univers que contenen a l'anterior i estan tancats baix constructors de tipos: ${𝒰}_1:\mathrm{...}:{𝒰}_{𝒾}:\mathrm{...}$

Aixina, podem parlar d'identitat entre tipos, $A{=}_{{𝒰}_{𝒾}}B$, per a algun univers $A,B:{𝒰}_{𝒾}$. L'identitat entre tipos, és dir, un camí entre espais, poden interpretar-se gràcies a l'axioma de Univalencia que afirma que l'identitat entre tipos és equivalent a l'equivalència entre tipos.

Axioma de Univalencia

La noció d'equivalència de tipos en HoTT pot definir-se de moltes formes llògicament equivalents que, no obstant, són molt distintes com a tipos. Originalment, la semàntica categòrica de Awodey i Warren interpreta l'equivalència de tipos com l'equivalència homotópica entre espais topològics. Aixina, diem que dos tipos són equivalents, $X\simeq Y$ si existixen dos funcions contínues $f:X\to Y,g:Y\to X$ tal que $f\circ g\sim 1_Y$ i $g\circ f\sim 1_X$, a on $\varphi \sim \psi$ significa que abdós funcions són homotópicas, i a on $1_X$ s'entén com el morfismo identitat de $X$, i.i. $1_X:X\to X$ tal que $1_X(x)=x,\mathrm{\forall }x:X.$

En definir la noció d'equivalència, podem notar que existix una forma canònica de convertir camins en equivalència; és dir, existix una funció del tipo

$(A=B)\to (A\simeq B),$

expressant que dos tipos A i B que són iguals són, en particular, equivalents.

El axioma de Univalencia declara que esta funció que acabem de definir és una equivalència en sí mateixa. És dir, tenim que

$(A=B)\simeq (A\simeq B).$

En atres paraules, l'igualtat és equivalent a l'equivalència. Podem considerar dos tipos equivalents són iguals.

Segons Awodey, açò implica que l'axioma de Univalencia reflectix la pràctica estructuralista de considerar objectes isomòrfics com a idèntics, ya que un isomorfisme es definix de forma anàloga a l'equivalència homotópica: $f:X\to Y,g:Y\to X$ tal que $f\circ g=1_Y$ i $g\circ f=1_X$. No obstant, no és clar que la definició d'isomorfisme de tipos en HoTT puga ser compatible en l'axioma de Univalencia, com discutixen James Ladyman i Stuart Presnell (2019).