Homotopi typteori

Omslag till Homotopy Type Theory: Univalent Foundations of Mathematics .

Inom matematisk logik och datavetenskap hänvisar homotopitypteori ( HoTT / h ɒ t / ) till olika utvecklingslinjer för intuitionistisk typteori , baserat på tolkningen av typer som objekt för vilka intuitionen av (abstrakt) homotopi-teorin gäller.

Detta inkluderar, bland andra arbetslinjer, konstruktionen av homotopiska och högre kategoriska modeller för sådana typteorier; användningen av typteori som logik (eller internt språk ) för abstrakt homotopiteori och högre kategoriteori ; utvecklingen av matematik inom en typteoretisk grund (inklusive både tidigare existerande matematik och ny matematik som homotopiska typer möjliggör); och formaliseringen av var och en av dessa i datorsäkra assistenter .

Det finns en stor överlappning mellan det arbete som kallas homotopitypteori och som det univalenta grundprojektet. Även om ingendera är exakt avgränsad, och termerna ibland används omväxlande, motsvarar valet av användning ibland också skillnader i synsätt och betoning. Som sådan representerar denna artikel kanske inte alla forskares åsikter på samma sätt. Denna typ av variation är oundviklig när ett fält är i snabb flux.

Historia

Förhistoria: groupoidmodellen

En gång i tiden var tanken att typer i intensional typteori med deras identitetstyper kunde betraktas som groupoider matematisk folklore . Den preciserades först semantiskt i Martin Hofmanns och Thomas Streichers uppsats från 1994 , kallad "The groupoid model refutes uniqueness of identity proofs", där de visade att intensional typteori hade en modell i kategorin groupoids . Detta var den första verkligt " homotopiska " modellen av typteorin, om än bara "1- dimensionell " (de traditionella modellerna i kategorin mängder är homotopiskt 0-dimensionella).

Deras uppföljningsdokument förebådade flera senare utvecklingar inom homotopitypteori. Till exempel noterade de att groupoidmodellen uppfyller en regel som de kallade "universumextensionalitet", vilket är ingen annan än begränsningen till 1-typer av univalensaxiomet som Vladimir Voevodsky föreslog tio år senare. (Axiomet för 1-typer är dock anmärkningsvärt enklare att formulera, eftersom ett sammanhängande begrepp om "ekvivalens" inte krävs.) De definierade också "kategorier med isomorfism som jämlikhet" och antog att i en modell som använder högredimensionella gruppoider, för sådana kategorier skulle man ha "ekvivalens är jämlikhet"; detta bevisades senare av Benedikt Ahrens, Krzysztof Kapulkin och Michael Shulman .

Tidig historia: modellkategorier och högre gruppoider

De första högredimensionella modellerna av intensional typteori konstruerades av Steve Awodey och hans elev Michael Warren 2005 med hjälp av Quillen modellkategorier . Dessa resultat presenterades först offentligt vid konferensen FMCS 2006 där Warren höll ett föredrag med titeln "Homotopy models of intensional type theory", som också fungerade som hans avhandlingsprospekt (avhandlingskommittén som var närvarande var Awodey, Nicola Gambino och Alex Simpson). En sammanfattning finns i Warrens avhandlingsprospectus abstract.

Vid en efterföljande workshop om identitetstyper vid Uppsala universitet 2006 hölls två föredrag om relationen mellan intensional typteori och faktoriseringssystem: ett av Richard Garner, "Factorization systems for type theory", och ett av Michael Warren, "Modelkategorier och intensiva identitetstyper". Relaterade idéer diskuterades i samtalen av Steve Awodey, "Typteori om högre dimensionella kategorier", och Thomas Streicher , "Identitetstyper vs. svaga omega-gruppoider: vissa idéer, vissa problem". Vid samma konferens höll Benno van den Berg ett föredrag med titeln "Typer som svaga omega-kategorier" där han beskrev de idéer som senare blev föremål för en gemensam artikel med Richard Garner.

Alla tidiga konstruktioner av högre dimensionella modeller var tvungna att hantera problemet med koherens typiskt för modeller av beroende typteori, och olika lösningar utvecklades. En sådan gavs 2009 av Voevodsky, en annan 2010 av van den Berg och Garner. En generell lösning, som bygger på Voevodskys konstruktion, gavs så småningom av Lumsdaine och Warren 2014.

På PSSL86 2007 höll Awodey ett föredrag med titeln "Homotopy type theory" (detta var den första offentliga användningen av den termen, som myntades av Awodey). Awodey och Warren sammanfattade sina resultat i artikeln "Homotopy theoretic models of identity types", som publicerades på ArXiv preprint-server 2007 och publicerades 2009; en mer detaljerad version dök upp i Warrens avhandling "Homotopy theoretic aspects of constructive type theory" 2008.

Vid ungefär samma tidpunkt undersökte Vladimir Voevodsky självständigt typteori i samband med sökandet efter ett språk för praktisk formalisering av matematik. I september 2006 skrev han till Typers e-postlista "En mycket kort anteckning om homotopi lambda-kalkyl ", som skisserade konturerna av en typteori med beroende produkter, summor och universum och av en modell av denna typteori i Kan simplicial set . Det började med att säga "The homotopy λ-calculus is a hypothetical (för tillfället) typ system" och slutade med "För tillfället är mycket av det jag sa ovan på nivån av gissningar. Även definitionen av modellen av TS i homotopikategorin är icke-trivial" med hänvisning till de komplexa koherensfrågorna som inte löstes förrän 2009. Denna anteckning inkluderade en syntaktisk definition av "jämlikhetstyper" som påstods tolkas i modellen av vägrum, men tog inte hänsyn till Per Martin-Löfs regler för identitetstyper. Det stratifierade också universum efter homotopidimension utöver storlek, en idé som senare mestadels förkastades.

På den syntaktiska sidan antog Benno van den Berg 2006 att tornet av identitetstyper av en typ i intensional typteori borde ha strukturen av en ω-kategori, och faktiskt en ω-gruppoid, i "globular, algebraisk" mening av Michael Batanin. Detta bevisades senare oberoende av van den Berg och Garner i tidningen "Types are weak omega-groupoids" (publicerad 2008) och av Peter Lumsdaine i tidningen "Weak ω-Categories from Intensional Type Theory" (publicerad 2009) och som del av hans 2010 Ph.D. avhandling "Högre kategorier från typteorier".

Univalensaxiomet, teorin om syntetisk homotopi och högre induktiva typer

Konceptet med en univalent fibration introducerades av Voevodsky i början av 2006. Men på grund av att alla presentationer av Martin-Löfs typteorin insisterade på egenskapen att identitetstyperna, i det tomma sammanhanget, bara kan innehålla reflexivitet, gjorde Voevodsky det erkänner inte förrän 2009 att dessa identitetstyper kan användas i kombination med de univalenta universum. Särskilt idén att univalens kan introduceras helt enkelt genom att lägga till ett axiom till den befintliga Martin-Löf-typteorin dök upp först 2009.

Även 2009 arbetade Voevodsky ut mer av detaljerna i en modell av typteori i Kan-komplex och observerade att existensen av en universell Kan-fibrering kunde användas för att lösa koherensproblemen för kategoriska modeller av typteori. Han bevisade också, med hjälp av en idé från AK Bousfield, att denna universella fibrering var univalent: den associerade fibreringen av parvisa homotopiekvivalenser mellan fibrerna är ekvivalent med basens banor-rymdfibrering.

För att formulera univalens som ett axiom hittade Voevodsky ett sätt att definiera "ekvivalenser" syntaktisk som hade den viktiga egenskapen att typen som representerar påståendet "f är en ekvivalens" var (under antagandet om funktionsextensionalitet) (-1)-trunkerad (dvs. sammandragbar om den är bebodd). Detta gjorde det möjligt för honom att ge ett syntaktisk uttalande om univalens, och generaliserade Hofmann och Streichers "universumextensionalitet" till högre dimensioner. Han kunde också använda dessa definitioner av ekvivalenser och sammandragbarhet för att börja utveckla betydande mängder "syntetisk homotopi-teori" i bevisassistenten Coq ; detta utgjorde grunden för biblioteket senare kallat "Foundations" och så småningom "UniMath".

Förenandet av de olika trådarna började i februari 2010 med ett informellt möte på Carnegie Mellon University , där Voevodsky presenterade sin modell i Kan-komplex och sin Coq för en grupp inklusive Awodey, Warren, Lumsdaine, Robert Harper , Dan Licata, Michael Shulman , och andra . Detta möte producerade konturerna av ett bevis (av Warren, Lumsdaine, Licata och Shulman) att varje homotopi-ekvivalens är en likvärdighet (i Voevodskys goda sammanhängande mening), baserat på idén från kategoriteorin om att förbättra likvärdigheter till sammanhängande ekvivalenser. Strax därefter bevisade Voevodsky att univalensaxiomet innebär funktionsextensionalitet.

Nästa centrala evenemang var en mini-workshop vid Mathematical Research Institute of Oberwolfach i mars 2011 anordnad av Steve Awodey, Richard Garner, Per Martin-Löf och Vladimir Voevodsky, med titeln "The homotopy interpretation of constructive type theory". Som en del av en Coq-handledning för denna workshop skrev Andrej Bauer ett litet Coq-bibliotek baserat på Voevodskys idéer (men använde faktiskt inte någon av hans kod); detta blev så småningom kärnan i den första versionen av "HoTT" Coq-biblioteket (den första commit av det senare av Michael Shulman noterar "Utveckling baserad på Andrej Bauers filer, med många idéer hämtade från Vladimir Voevodskys filer"). En av de viktigaste sakerna som kom ut från Oberwolfach-mötet var grundidén om högre induktiva typer, på grund av Lumsdaine, Shulman, Bauer och Warren. Deltagarna formulerade också en lista med viktiga öppna frågor, såsom om univalensaxiomet uppfyller kanonitet (fortfarande öppet, även om vissa specialfall har lösts positivt), om univalensaxiomet har icke-standardiserade modeller (sedan besvarats positivt av Shulman) och hur att definiera (semi)enkla typer (fortfarande öppen i MLTT, även om det kan göras i Voevodskys Homotopy Type System (HTS), en typteori med två likhetstyper).

Strax efter Oberwolfach-workshopen etablerades Homotopy Type Theory-webbplatsen och bloggen , och ämnet började populariseras under det namnet. En uppfattning om några av de viktiga framstegen under denna period kan fås från bloggens historia.

Univalenta grunder

Frasen "univalenta grunder" är av alla överens om att vara nära besläktad med teorin om homotopityp, men alla använder den inte på samma sätt. Det användes ursprungligen av Vladimir Voevodsky för att hänvisa till hans vision om ett grundläggande system för matematik där de grundläggande objekten är homotopityper, baserat på en typteori som uppfyller § univalensaxiomet och formaliserad i en datorsäker assistent.

När Voevodskys arbete blev integrerat med gemenskapen av andra forskare som arbetade med homotopitypteori, användes "univalent foundations" ibland omväxlande med "homotopitypteori", och andra gånger för att endast hänvisa till dess användning som ett grundsystem (exklusive t.ex. , studiet av modellkategorisk semantik eller beräkningsmetateori). Till exempel var ämnet för IAS specialår officiellt angett som "univalent foundations", även om mycket av arbetet som gjordes där fokuserade på semantik och metateori förutom stiftelser. Boken producerad av deltagare i IAS-programmet hade titeln "Homotopy type theory: Univalent foundations of mathematics"; även om detta kan hänvisa till endera användningen, eftersom boken bara diskuterar HoTT som en matematisk grund.

Specialår på Univalent Foundations of Mathematics

En animation som visar utvecklingen av HoTT-boken på GitHub-förvaret av deltagarna i Univalent Foundations Special Year-projektet.

2012–13 höll forskare vid Institutet för avancerade studier "A Special Year on Univalent Foundations of Mathematics". Det speciella året samlade forskare inom topologi , datavetenskap , kategoriteori och matematisk logik . Programmet organiserades av Steve Awodey , Thierry Coquand och Vladimir Voevodsky .

Under programmet initierade Peter Aczel , som var en av deltagarna, en arbetsgrupp som undersökte hur man gör typteori informellt men rigoröst, i en stil som är analog med vanliga matematiker som gör mängdlära. Efter inledande experiment stod det klart att detta inte bara var möjligt utan mycket fördelaktigt, och att en bok (den så kallade HoTT-boken ) kunde och borde skrivas. Många andra deltagare i projektet anslöt sig sedan till arbetet med teknisk support, skrivande, korrekturläsning och idéer. Ovanligt för en matematiktext utvecklades den i samarbete och i det fria på GitHub , släpps under en Creative Commons-licens som tillåter människor att punga sin egen version av boken och är både köpbar i tryckt form och nedladdningsbar gratis.

Mer allmänt var det speciella året en katalysator för hela ämnets utveckling; HoTT-boken var bara ett, om än det mest synliga, resultat.

Officiella deltagare i det speciella året

• Peter Aczel
• Benedikt Ahrens
• Thorsten Altenkirch
• Steve Awodey
• Bruno Barras
• Andrej Bauer
• Yves Bertot
• Marc Bezem
• Thierry Coquand
• Eric Finster
• Daniel Grayson
• Hugo Herbelin
• André Joyal
• Dan Licata
• Peter Lumsdaine
• Assia Mahboubi
• Per Martin-Löf
• Sergey Melikhov
• Alvaro Pelayo
• Andrew Polonsky
• Michael Shulman
• Matthieu Sozeau
• Bas Spitters
• Benno van den Berg
• Vladimir Voevodsky
• Michael Warren
• Noam Zeilberger

ACM Computing Reviews listade boken som en anmärkningsvärd 2013-publikation i kategorin "mathematics of computing".

Nyckelbegrepp

Intentionell typteori	Homotopi teori
typer $A$	blanksteg $A$
termer $a$	pekar $a$
$a:A$	$a\in A$
beroende typ $x:A\ \vdash \ B(x)\$	fibration $B\to A$
identitetstyp $\mathrm {Id} _{A}(a,b)$	väg utrymme
$p:\mathrm {Id} _{A}(a,b)$	sökväg $p:a\to b$
$\alpha :\mathrm {Id} _{\mathrm {Id} _{A}(a,b)}(p,q)$	homotopi $\alpha :p\Högerpil q$

"Propositioner som typer"

HoTT använder en modifierad version av " propositioner som typer " tolkningen av typteorin, enligt vilken typer också kan representera propositioner och termer sedan kan representera bevis. I HoTT spelas emellertid, till skillnad från i vanliga "propositioner som typer", en speciell roll av "bara propositioner", som grovt sett är de typer som har högst en term, upp till propositionell likhet . Dessa är mer som konventionella logiska propositioner än allmänna typer, eftersom de är bevis-irrelevanta.

Jämlikhet

Det grundläggande konceptet för teorin om homotopityp är vägen . I HoTT är typen $a=b$ typen av alla vägar från punkten $a$ till punkten $b$ . (Därför är ett bevis på att en punkt ${\displaystyle a} är$ lika med en punkt $b$ samma sak som en bana från punkten $a$ till punkten $b$ .) För varje punkt $a$ , finns det en väg av typen $a=a$ , motsvarande den reflexiva egenskapen för likhet. En bana av typen $a=b$ kan inverteras och bilda en bana av typen $b=a$ , motsvarande den symmetriska egenskapen för likhet. Två sökvägar av typen $a=b$ resp. $b=c$ kan sammanfogas och bildar en sökväg av typen $a=c$ ; detta motsvarar den transitiva egenskapen jämlikhet.

Viktigast av allt, givet en sökväg $p:a=b$ och ett bevis på någon egenskap $P(a)$ , kan beviset "transporteras" längs vägen $p$ för att ge ett bevis på egenskapen $P(b)$ . (Ekvivalent uttryckt, ett objekt av typen $P(a)$ kan förvandlas till ett objekt av typen $P(b)$ .) Detta motsvarar egenskapen substitut av likhet . Här kommer en viktig skillnad mellan HoTT och klassisk matematik in. I klassisk matematik, när likheten mellan två värden $a$ och $b$ har fastställts, $a$ och ${\ displaystyle b}$ kan användas omväxlande därefter, utan hänsyn till någon skillnad mellan dem. I teorin om homotopityp kan det dock finnas flera olika vägar $a=b$ , och transport av ett objekt längs två olika vägar kommer att ge två olika resultat. I teorin om homotopityp är det därför nödvändigt att ange vilken väg som används vid tillämpning av substitutionsegenskapen.

I allmänhet kan en "proposition" ha flera olika bevis. (Till exempel, typen av alla naturliga tal, när den betraktas som en proposition, har varje naturligt tal som ett bevis.) Även om en proposition bara har ett bevis $a$ , är utrymmet för banorna ${\ displaystyle a=a}$ kan vara icke-trivial på något sätt. En "bara proposition" är vilken typ som helst som antingen är tom eller bara innehåller en punkt med ett trivialt sökvägsutrymme .

Observera att folk skriver $a=b$ för $Id_{A}(a,b)$ , och lämnar därmed typ $A$ av $a,b$ implicit. Förväxla det inte med ${\displaystyle id_{A}:A\to A} ,$ som anger identitetsfunktionen på $A$ .

Typekvivalens

Två typer $A$ och $B$ som tillhör något universum $U$ definieras som likvärdiga om det finns en ekvivalens mellan dem. En ekvivalens är en funktion

$f:A\to B$

som har både en vänsterinvers och en högerinvers, i den meningen att för lämpligt valda $g$ och $h$ , är följande typer båda bebodda:

$Id_{B\rightarrow B}(f\circ g,id_{B}),$

$Id_{A\rightarrow A}(h\circ f,id_{A}).$

dvs

$f\circ g=_{B\rightarrow B}id_{B},$

$h\circ f=_{A\rightarrow A}id_{A}.$

Detta uttrycker en allmän uppfattning om " $f$ har både en vänsterinvers och en högerinvers", med hjälp av likhetstyper. Observera att inverterbarhetsvillkoren ovan är likhetstyper i funktionstyperna $A\rightarrow A$ och $B\rightarrow B$ . Man antar generellt funktionen extensionality axiom, som säkerställer att dessa är ekvivalenta med följande typer som uttrycker inverterbarhet med hjälp av likheten på domänen och koddomänen $A$ och $B$ :

$\Pi _{y:B}.\ Id_{B}((f\circ g)(y),id_ {B}(y)),$

$\Pi _{x:A}.\ Id_{A}((h\circ f)(x),id_{A}(x)).$

dvs för alla $x:A$ och $y:B$ ,

$f(g(y))=_{B}y,$

$h(f(x))=_{A}x.$

Typens funktioner

$A\to B$

tillsammans med ett bevis på att de är likvärdiga betecknas med

$A\simeq B$ .

Univalensaxiomet

Efter att ha definierat funktioner som är ekvivalenser enligt ovan kan man visa att det finns ett kanoniskt sätt att vända vägar till ekvivalenser. Det finns med andra ord en funktion av typen

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

vilket uttrycker att typerna $A,B$ som är lika i synnerhet också är ekvivalenta.

Univalensaxiomet säger att denna funktion i sig är en ekvivalens . Därför har vi

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

"Med andra ord, identitet är ekvivalent med ekvivalens. I synnerhet kan man säga att "likvärdiga typer är identiska".

Martín Hötzel Escardó har visat att egenskapen univalens "är obestämd i Martin-Löf Type Theory (MLTT)".

Ansökningar

Sats bevisar

Förespråkarna hävdar att HoTT tillåter att matematiska bevis översätts till ett datorprogrammeringsspråk för datorkorrekturassistenter mycket lättare än tidigare. De hävdar att detta tillvägagångssätt ökar möjligheten för datorer att kontrollera svåra bevis. Dessa påståenden är dock inte allmänt accepterade och många forskningsinsatser och bevisassistenter använder sig inte av HoTT.

HoTT antar univalensaxiomet, som relaterar likheten mellan logiskt-matematiska propositioner till homotopi-teori. En ekvation som "a=b" är en matematisk proposition där två olika symboler har samma värde. I teorin om homotopityp anses detta betyda att de två formerna som representerar symbolernas värden är topologiskt ekvivalenta.

Dessa ekvivalensförhållanden, hävdar ETH Zürich Institute for Theoretical Studies direktör Giovanni Felder , kan formuleras bättre i homotopiteorin eftersom de är mer omfattande: Homotopi teorin förklarar inte bara varför "a är lika med b" utan också hur man härleder detta. I mängdteorin skulle denna information behöva definieras ytterligare, vilket, hävdar förespråkarna, gör översättningen av matematiska propositioner till programmeringsspråk svårare.

Dataprogramering

Från och med 2015 pågick ett intensivt forskningsarbete för att modellera och formellt analysera beräkningsbeteendet för univalensaxiomet i teorin om homotopityp.

Kubisk typteori är ett försök att ge beräkningsinnehåll till teori om homotopityp.

Man tror dock att vissa objekt, såsom semi-enkla typer, inte kan konstrueras utan hänvisning till någon föreställning om exakt jämlikhet. Därför har olika typteorier på två nivåer utvecklats som delar upp sina typer i fibranttyper, som respekterar banor, och icke-fibranttyper, som inte gör det. Kartesisk kubisk beräkningstypteori är den första tvånivåtypteorin som ger en fullständig beräkningstolkning av homotopitypteori.

Se även

• Beräkning av konstruktioner
• Curry–Howard korrespondens
• Intuitionistisk typteori
• Homotopihypotes
• Univalenta grunder

Bibliografi

•   Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics . Princeton, NJ: Institutet för avancerade studier . MR 3204653 . ( GitHub-versionen citerad i den här artikeln.)
•   Awodey, S. ; Warren, MA (januari 2009). "Homotopi-teoretiska modeller av identitetstyper". Mathematical Proceedings of the Cambridge Philosophical Society . 146 (1): 45–55. arXiv : 0709.0248 . Bibcode : 2008MPCPS.146...45A . doi : 10.1017/S0305004108001783 . S2CID 7915709 . Som PDF .
•     Awodey, Steve (2012). "Typteori och homotopi" (PDF) . I Dybjer, P.; Lindström, Sten; Palmgren, Erik; et al. (red.). Epistemologi kontra ontologi . Logik, epistemologi och vetenskapens enhet. Springer. s. 183–201. CiteSeerX 10.1.1.750.3626 . doi : 10.1007/978-94-007-4435-6_9 . ISBN 978-94-007-4434-9 . S2CID 4499538 .
•   Awodey, Steve (2014). "Strukturalism, invarians och univalens". Philosophia Mathematica . 22 (1): 1–11. CiteSeerX 10.1.1.691.8113 . doi : 10.1093/philmat/nkt030 .
•   Hofmann, Martin; Streicher, Thomas (1998). "Den gruppoida tolkningen av typteorin" . I Sambin, G.; Smith, JM (red.). Tjugofem år av konstruktiv typteori . Clarendon Press. s. 83–112. ISBN 978-0-19-158903-4 . Som efterskrift .
• Rijke, Egbert (2012). Homotopy Type Theory (PDF) (Master's). Utrecht universitet.
• Voevodsky, Vladimir (2006), En mycket kort anteckning om Homotopy Lambda Calculus (PDF)
• Voevodsky, Vladimir (2010), The Equivalence Axiom and Univalent Models of Type Theory , arXiv : 1402.5556 , Bibcode : 2014arXiv1402.5556V
• Warren, Michael A. (2008). Homotopi Theoretic Aspects of Constructive Type Theory (PDF) (Ph.D.). Carnegie Mellon University.

Vidare läsning

• David Corfield (2020), Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy , Oxford University Press.
• Egbert Rijke (2022), Introduktion till homotopitypteori , arXiv : 2212.11082 . Inledande lärobok.

externa länkar

• Homotopi typteori
• Homotopi typteori vid n Lab
• Homotopi typ teori wiki
• Vladimir Voevodskys webbsida om Univalent Foundations
• Homotopy Type Theory and the Univalent Foundations of Mathematics av ​​Steve Awodey
• "Constructive Type Theory and Homotopy" – Videoföreläsning av Steve Awodey vid Institute for Advanced Study

Bibliotek för formaliserad matematik

• Foundations bibliotek (2010-nuvarande)
• HoTT-bibliotek (2011-nuvarande) 30 januari 2022
• P-adics bibliotek (2011-2012)
• RezkCompletion bibliotek , januari 2022 (nu integrerat i UniMath, där vidareutveckling sker)
• Ktheory bibliotek
• UniMath-biblioteket (2014-nuvarande) , 25 januari 2022