Teoria typów homotopii - Homotopy type theory

Okładka teorii typów homotopii: jednowartościowe podstawy matematyki .

W logice matematycznej i informatyki , teoria homotopii typ ( HoTT / h ɒ t / ) odnosi się do różnych linii rozwoju intuicjonistycznej teorii typów , na podstawie interpretacji typów jako obiekty do których intuicja (streszczenie) teorii homotopii zastosowanie.

Obejmuje to między innymi budowę modeli homotopicznych i wyżej kategorycznych dla teorii tego typu; wykorzystanie teorii typów jako logiki (lub języka wewnętrznego ) dla abstrakcyjnej teorii homotopii i teorii wyższych kategorii ; rozwój matematyki w ramach podstaw teorii typów (obejmujących zarówno matematykę istniejącą wcześniej, jak i nową, którą umożliwiają typy homotopowe); i sformalizowanie każdego z nich w asystentach komputerowych .

Praca określana jako teoria typu homotopii w dużym stopniu pokrywa się z projektem podstaw jednowartościowych . Chociaż żadne z nich nie jest precyzyjnie nakreślone, a terminy są czasami używane zamiennie, to wybór użycia odpowiada również czasami różnicom w punkcie widzenia i akcentowaniu. Jako taki, ten artykuł może nie reprezentować w równym stopniu poglądów wszystkich badaczy w tych dziedzinach. Tego rodzaju zmienność jest nieunikniona, gdy pole jest w szybkim ruchu.

Historia

Prehistoria: model groupoid

Kiedyś idea, że ​​typy w teorii typów intensjonalnych wraz z ich typami tożsamości mogą być uważane za grupoidy, była matematycznym folklorem . Po raz pierwszy została ona sprecyzowana semantycznie w pracy z 1998 r. Martina Hofmanna i Thomasa Streichera zatytułowanej „The groupoid interpretation of type teoria”, w której wykazali, że intensjonalna teoria typów ma model w kategorii grupoidów . Był to pierwszy prawdziwie „ homotopiczny ” model teorii typów, aczkolwiek tylko „ jednowymiarowy ” (tradycyjne modele w kategorii zbiorów są homotopicznie 0-wymiarowe).

Ich artykuł zapowiadał również kilka późniejszych zmian w teorii typów homotopii. Zauważyli na przykład, że model groupoid spełnia regułę, którą nazwali „wszechświatową ekstensjonalnością”, która jest niczym innym jak ograniczeniem do typu 1 aksjomatu jednoznaczności , zaproponowanym dziesięć lat później przez Vladimira Voevodsky'ego . (Aksjomat dla typów 1 jest jednak znacznie prostszy do sformułowania, ponieważ spójne pojęcie „równoważności” nie jest wymagane.) Zdefiniowali również „kategorie z izomorfizmem jako równością” i wywnioskowali, że w modelu wykorzystującym grupoidy o wyższych wymiarach, dla takich kategorii mielibyśmy „równoważność to równość”; udowodnili to później Benedikt Ahrens, Krzysztof Kapulkin i Michael Shulman .

Wczesna historia: kategorie modeli i wyższe groupoidy

Pierwsze wielowymiarowe modele teorii typów intensjonalnych zostały skonstruowane przez Steve'a Awodeya i jego ucznia Michaela Warrena w 2005 roku przy użyciu kategorii modeli Quillena . Wyniki te zostały po raz pierwszy zaprezentowane publicznie na konferencji FMCS 2006, na której Warren wygłosił referat zatytułowany „Modele homotopii teorii typów intensjonalnych”, który posłużył również jako prospekt jego pracy (obecni komisja dysertacyjna to Awodey, Nicola Gambino i Alex Simpson). Podsumowanie zawarte jest w streszczeniu prospektu pracy magisterskiej Warrena.

Na kolejnych warsztatach poświęconych typom tożsamości na Uniwersytecie w Uppsali w 2006 r. odbyły się dwa wykłady na temat relacji między teorią typów intensjonalnych a systemami faktoryzacji: jedno Richarda Garnera „Systemy faktoryzacji dla teorii typów” i drugie Michaela Warrena „Kategorie modeli i intensjonalne typy tożsamości”. Powiązane idee zostały omówione w wystąpieniach Steve'a Awodeya „Teoria typów kategorii wyższych wymiarów” i Thomasa Streichera „Typy tożsamości a słabe grupy omega: niektóre pomysły, niektóre problemy”. Na tej samej konferencji Benno van den Berg wygłosił wykład zatytułowany „Typy jako słabe kategorie omega”, w którym przedstawił idee, które później stały się tematem wspólnego artykułu z Richardem Garnerem.

Wszystkie wczesne konstrukcje modeli wysokowymiarowych musiały radzić sobie z problemem koherencji typowym dla modeli teorii typów zależnych i opracowano różne rozwiązania. Jeden taki podarował w 2009 roku Wojewodski, inny w 2010 roku van den Berg i Garner. Ogólne rozwiązanie, oparte na konstrukcji Voevodsky'ego, zostało ostatecznie podane przez Lumsdaine'a i Warrena w 2014 roku.

Na PSSL86 w 2007 roku Awodey wygłosił referat zatytułowany „Teoria typu homotopii” (było to pierwsze publiczne użycie tego terminu, który został ukuty przez Awodeya). Awodey i Warren podsumowali swoje wyniki w artykule „Teoretyczne modele homotopii typów tożsamości”, który został opublikowany na serwerze preprintu ArXiv w 2007 roku i opublikowany w 2009 roku; bardziej szczegółowa wersja pojawiła się w pracy Warrena „Teoretyczne aspekty homotopii teorii typów konstruktywnych” w 2008 roku.

Mniej więcej w tym samym czasie Władimir Wojewodski niezależnie badał teorię typów w kontekście poszukiwań języka do praktycznej formalizacji matematyki. We wrześniu 2006 wysłał na listę dyskusyjną Types "Bardzo krótką notatkę na temat rachunku homotopii lambda ", w której naszkicował zarys teorii typów z iloczynami zależnymi, sumami i wszechświatami oraz model tej teorii typów w prostych zbiorach Kan . Zaczęło się od stwierdzenia „Rachunek λ homotopii jest hipotetycznym (w tej chwili) systemem typu” i zakończyło się „W tej chwili wiele z tego, co powiedziałem powyżej, jest na poziomie przypuszczeń. Nawet definicja modelu TS w kategoria homotopii jest nietrywialna” odnosząc się do złożonych kwestii koherencji, które nie zostały rozwiązane do 2009 roku. Notatka ta zawierała definicję syntaktyczną „typów równości”, które miały być interpretowane w modelu przez przestrzenie ścieżek, ale nie uwzględniono Według reguł Martina-Löfa dla typów tożsamości. Oprócz rozmiaru podzielił on także wszechświaty według wymiaru homotopii, co później w większości zostało odrzucone.

Jeśli chodzi o składnię, Benno van den Berg przypuszczał w 2006 roku, że wieża typów tożsamościowych typu w teorii typów intensjonalnych powinna mieć strukturę ω-kategorii, a nawet ω-groupoidy, w sensie „globalnym, algebraicznym”. Michaela Batanina. Zostało to później udowodnione niezależnie przez van den Berga i Garnera w artykule „Typy są słabymi grupami omega” (opublikowane w 2008 roku) oraz przez Petera Lumsdaine w artykule „Weak ω-Categories from Intensional Type Theory” (opublikowany w 2009 roku) oraz jako część jego doktoratu z 2010 r. praca magisterska „Wyższe kategorie z teorii typów”.

Aksjomat jednowartościowości, syntetyczna teoria homotopii i wyższe typy indukcyjne

Pojęcie jednowartościowego rozwłóknienia zostało wprowadzone przez Wojewodskiego na początku 2006 roku. Jednak ze względu na nacisk we wszystkich prezentacjach teorii typów Martina-Löfa na własność, że typy tożsamościowe, w pustym kontekście, mogą zawierać tylko refleksyjność, Wojewodski to zrobił. nie rozpoznać do 2009 roku, że te typy tożsamości mogą być używane w połączeniu z uniwalentnymi wszechświatami. W szczególności pomysł, że jednoznaczność można wprowadzić po prostu przez dodanie aksjomatu do istniejącej teorii typu Martina-Löfa, pojawił się dopiero w 2009 roku.

Również w 2009 roku Voevodsky opracował więcej szczegółów modelu teorii typów w kompleksach Kan i zaobserwował, że istnienie uniwersalnej fibracji Kan może być wykorzystane do rozwiązania problemów z koherencją modeli kategorycznych teorii typów. Udowodnił również, posługując się pomysłem AK Bousfielda, że ​​ta uniwersalna fibracja była jednowartościowa: skojarzone fibrowanie równoważności parami homotopii między włóknami jest równoważne fibracji ścieżka-przestrzeń podstawy.

Aby sformułować jednoznaczność jako aksjomat, Wojewodsky znalazł sposób na syntaktyczne zdefiniowanie „równoważności”, który miał tę ważną właściwość, że typ reprezentujący zdanie „f jest równoważnością” był (przy założeniu ekstensjonalności funkcji) (-1) – obcięty (tj. kurczliwy, jeśli jest zamieszkany). Umożliwiło mu to sformułowanie syntaktycznego stwierdzenia jednoznaczności, uogólniając „wszechświatową ekstensjonalność” Hofmanna i Streichera na wyższe wymiary. Był również w stanie użyć tych definicji równoważności i kurczliwości, aby zacząć rozwijać znaczne ilości „syntetycznej teorii homotopii” w asystencie dowodu Coq ; to stanowiło podstawę biblioteki nazwanej później „Fundacjami” i ostatecznie „UniMath”.

Ujednolicenie różnych wątków rozpoczęło się w lutym 2010 roku nieformalnym spotkaniem na Uniwersytecie Carnegie Mellon , gdzie Voevodsky zaprezentował swój model w kompleksach Kan i swój kod Coq grupie obejmującej Awodey, Warren, Lumsdaine i Robert Harper , Dan Licata, Michael Shulman , i inni. Spotkanie to przyniosło zarys dowodu (opracowanego przez Warrena, Lumsdaine'a, Licatę i Shulmana), że każda równoważność homotopii jest równoważnością (w dobrym spójnym sensie Wojewodzkiego), w oparciu o koncepcję z teorii kategorii ulepszania równoważności do równoważności sąsiadujących. Wkrótce potem Wojewodski dowiódł, że aksjomat jednowartościowości implikuje ekstensjonalność funkcji.

Kolejnym kluczowym wydarzeniem były mini-warsztaty w Mathematical Research Institute of Oberwolfach w marcu 2011 r. zorganizowane przez Steve'a Awodeya, Richarda Garnera, Pera Martina-Löfa i Vladimira Voevodsky'ego, zatytułowane "Homotopowa interpretacja teorii typu konstruktywnego". W ramach samouczka Coq dla tego warsztatu, Andrej Bauer napisał małą bibliotekę Coq opartą na pomysłach Voevodsky'ego (ale w rzeczywistości nie używając żadnego z jego kodu); to ostatecznie stało się jądrem pierwszej wersji biblioteki Coq „HoTT” (pierwsze zatwierdzenie tej ostatniej autorstwa Michaela Shulmana zauważa „Rozwój oparty na plikach Andreja Bauera, z wieloma pomysłami zaczerpniętymi z plików Vladimira Voevodsky'ego”). Jedną z najważniejszych rzeczy, które wyłoniły się ze spotkania w Oberwolfach, była podstawowa idea wyższych typów indukcyjnych, ze względu na Lumsdaine'a, Shulmana, Bauera i Warrena. Uczestnicy sformułowali również listę ważnych pytań otwartych, takich jak: czy aksjomat jednowartościowości spełnia kanoniczność (nadal otwarta, chociaż niektóre szczególne przypadki zostały rozwiązane pozytywnie), czy aksjomat jednowartościowości ma niestandardowe modele (ponieważ Shulman odpowiedział pozytywnie) oraz w jaki sposób zdefiniować typy (pół)proste (wciąż otwarte w MLTT, chociaż można to zrobić w Homotopy Type System (HTS) Voevodsky'ego, czyli teorii typów z dwoma typami równości).

Wkrótce po warsztatach Oberwolfach powstała strona internetowa i blog Homotopy Type Theory , a temat zaczął być popularyzowany pod tą nazwą. Wyobrażenie o niektórych ważnych postępach w tym okresie można uzyskać z historii bloga.

Fundamenty jednowartościowe

Wszyscy zgadzają się, że wyrażenie „uniwalentne podstawy” jest blisko związane z teorią typu homotopii, ale nie wszyscy używają go w ten sam sposób. Pierwotnie był używany przez Vladimira Voevodsky'ego w odniesieniu do jego wizji fundamentalnego systemu matematyki, w którym podstawowymi obiektami są typy homotopii, oparte na teorii typów spełniającej aksjomat jednowartościowości i sformalizowane w asystencie dowodzenia komputerowego.

Ponieważ prace Wojewodskiego zostały zintegrowane ze społecznością innych badaczy zajmujących się teorią typu homotopii, „podstawy jednowartościowe” były czasami używane zamiennie z „teorią typu homotopii”, a innym razem odnosiły się tylko do jej użycia jako systemu fundamentalnego (z wyłączeniem np. , badanie semantyki modelowo-kategorycznej lub metateorii obliczeniowej). Na przykład temat roku specjalnego IAS został oficjalnie podany jako „uniwalentne podstawy”, chociaż wiele prac tam wykonanych koncentrowało się nie tylko na podstawach, ale także na semantyce i metateorii. Książka przygotowana przez uczestników programu IAS nosiła tytuł „Teoria typów homotopii: Jednowartościowe podstawy matematyki”; chociaż może to odnosić się do obu zastosowań, ponieważ książka omawia tylko HoTT jako podstawę matematyczną.

Specjalny Rok Jednowartościowych Podstaw Matematyki

Odtwórz multimedia

Animacja przedstawiająca rozwój Księgi HoTT w repozytorium GitHub przez uczestników projektu Specjalnego Roku Univalent Foundations.

W latach 2012–13 naukowcy z Instytutu Badań Zaawansowanych zorganizowali „Specjalny Rok Jednowartościowych Podstaw Matematyki”. Ten szczególny rok zgromadził badaczy topologii , informatyki , teorii kategorii i logiki matematycznej . Program zorganizowali Steve Awodey , Thierry Coquand i Vladimir Voevodsky .

Podczas programu Peter Aczel , który był jednym z uczestników, zainicjował grupę roboczą, która badała, jak uprawiać teorię typów nieformalnie, ale rygorystycznie, w stylu analogicznym do zwykłych matematyków uprawiających teorię mnogości. Po wstępnych eksperymentach stało się jasne, że jest to nie tylko możliwe, ale i bardzo korzystne, i że książka (tzw. Książka HoTT ) może i powinna zostać napisana. Wielu innych uczestników projektu połączyło się następnie ze wsparciem technicznym, pisaniem, korektą i oferowaniem pomysłów. Co nietypowe dla tekstu matematycznego, został opracowany wspólnie i otwarty na GitHub , jest udostępniany na licencji Creative Commons, która pozwala ludziom na rozwidlenie własnej wersji książki i można ją kupić w wersji drukowanej i pobrać bezpłatnie.

Ogólnie rzecz biorąc, ten specjalny rok był katalizatorem rozwoju całego tematu; Księga HoTT była tylko jednym, choć najbardziej widocznym wynikiem.

Oficjalni uczestnicy w specjalnym roku

ACM Computing Reviews uznał tę książkę za godną uwagi publikację w 2013 roku w kategorii „matematyka informatyki”.

Kluczowe idee

Teoria typu intensjonalnego	Teoria homotopii
typy ${\ Displaystyle A}$	spacje ${\ Displaystyle A}$
warunki ${\displaystyle a}$	zwrotnica ${\displaystyle a}$
${\displaystyle a:A}$	${\displaystyle a\w A}$
typ zależny ${\ Displaystyle x: A \ \ vdash \ B (x) \ }$	fibracja ${\ Displaystyle B \ do A}$
typ tożsamości ${\ Displaystyle \ operatorname {identyfikator} _ {A} (a, b)}$	przestrzeń ścieżki
${\ Displaystyle p: \ operatorname {identyfikator} _ {A} (a, b)}$	ścieżka ${\displaystyle p:a\dob}$
${\ Displaystyle \ alfa : \ operatorname {identyfikator} _ {\ operatorname {identyfikator} _ {A} (a, b)} (p, q)}$	homotopia ${\ Displaystyle \ alfa : p \ Strzałka w prawo q}$

„Propozycje jako typy”

HoTT wykorzystuje zmodyfikowaną wersję interpretacji teorii typów „ zdań jako typów ”, zgodnie z którą typy mogą również reprezentować zdania, a terminy mogą następnie reprezentować dowody. Jednak w HoTT, w przeciwieństwie do standardowych „sądów jako typów”, szczególną rolę odgrywają „zwykłe zdania”, które z grubsza są typami posiadającymi co najwyżej jeden termin, aż do równości zdań . Przypominają one bardziej konwencjonalne zdania logiczne niż typy ogólne, ponieważ nie mają znaczenia dla dowodu.

Równość

Podstawowym pojęciem teorii typów homotopii jest ścieżka . W HoTT type jest typem wszystkich ścieżek od punktu do punktu . (Dlatego dowód, że punkt jest równy punktowi jest tym samym, co ścieżka z punktu do punktu .) Dla każdego punktu istnieje ścieżka typu , odpowiadająca zwrotnej własności równości. Ścieżkę typu można odwrócić, tworząc ścieżkę typu , odpowiadającą symetrycznej właściwości równości. Dwie ścieżki typu ew. można łączyć, tworząc ścieżkę typu ; odpowiada to przechodniej własności równości. ${\displaystyle a=b}$${\displaystyle a}$${\displaystyle b}$${\displaystyle a}$${\displaystyle b}$${\displaystyle a}$${\displaystyle b}$${\displaystyle a}$${\displaystyle a=a}$${\displaystyle a=b}$${\displaystyle b=a}$${\displaystyle a=b}$${\displaystyle b=c}$${\displaystyle a=c}$

Co najważniejsze, biorąc pod uwagę ścieżkę i dowód pewnej właściwości , dowód można „przetransportować” wzdłuż ścieżki, aby uzyskać dowód właściwości . (Mówiąc równoważnie, obiekt typu może zostać przekształcony w obiekt typu .) Odpowiada to własności substytucji równości . W tym miejscu pojawia się ważna różnica między HoTT a matematyką klasyczną. W matematyce klasycznej, gdy równość dwóch wartości i została ustalona i może być później używana zamiennie, bez względu na jakiekolwiek rozróżnienie między nimi. Jednak w teorii typów homotopii może istnieć wiele różnych ścieżek , a transport obiektu dwiema różnymi ścieżkami da dwa różne wyniki. Dlatego w teorii typów homotopii, stosując właściwość podstawienia, konieczne jest określenie, która ścieżka jest używana. ${\displaystyle p:a=b}$${\ Displaystyle P (a)}$${\displaystyle p}$${\ Displaystyle P (b)}$${\ Displaystyle P (a)}$${\ Displaystyle P (b)}$${\displaystyle a}$${\displaystyle b}$${\displaystyle a}$${\displaystyle b}$${\displaystyle a=b}$

Ogólnie rzecz biorąc, „stwierdzenie” może mieć wiele różnych dowodów. (Na przykład typ wszystkich liczb naturalnych, gdy jest rozpatrywany jako zdanie, ma każdą liczbę naturalną jako dowód.) Nawet jeśli zdanie ma tylko jeden dowód , przestrzeń ścieżek może być w pewien sposób nietrywialna. „Zwykła propozycja” to dowolny typ, który jest albo pusty, albo zawiera tylko jeden punkt z trywialną przestrzenią ścieżki . ${\displaystyle a}$${\displaystyle a=a}$

Zauważ, że ludzie piszą o tym samym pozostawiając typ z niejawny. Nie myl go z , oznaczającym funkcję tożsamości na . ${\displaystyle a=b}$${\ Displaystyle Id_ {A} (a, b)}$${\ Displaystyle A}$${\displaystyle a,b}$${\ Displaystyle id_ {A}: A \ do A}$${\ Displaystyle A}$

Równoważność typu

Dwa typy i przynależność do jakiegoś wszechświata są definiowane jako równoważne, jeśli istnieje między nimi równoważność . Równoważność to funkcja ${\ Displaystyle A}$${\ Displaystyle B}$${\ Displaystyle U}$

${\ Displaystyle f: A \ do B}$

który ma zarówno lewą odwrotność, jak i prawą odwrotność, w tym sensie, że dla odpowiednio dobranego i , zamieszkane są oba następujące typy: ${\displaystyle g}$${\ Displaystyle h}$

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

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

tj

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

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

Wyraża to ogólne pojęcie " ma zarówno lewą, jak i prawą odwrotność", używając typów równości. Zauważ, że powyższe warunki odwracalności są typami równości w typach funkcji i . Ogólnie przyjmuje się aksjomat ekstensjonalizmu funkcji, który zapewnia, że ​​są one równoważne z następującymi typami, które wyrażają odwracalność za pomocą równości w dziedzinie i kodziedzinie oraz : ${\displaystyle f}$${\displaystyle A\rightarrow A}$${\displaystyle B\rightarrow B}$${\ Displaystyle A}$${\ Displaystyle B}$

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

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

czyli dla wszystkich i , ${\displaystyle x:A}$${\displaystyle y:B}$

${\ Displaystyle f (g (y)) = _ {B} y}$

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

Funkcje typu

${\ Displaystyle A \ do B}$

wraz z dowodem, że są to równoważności oznaczone są przez

${\ Displaystyle A \ Simeq B}$.

Aksjomat jednoznaczności

Mając zdefiniowane funkcje, które są równoważnościami jak wyżej, można wykazać, że istnieje kanoniczny sposób zawracania ścieżek do równoważności. Innymi słowy, istnieje funkcja typu

${\ Displaystyle (A = B) \ do (A \ Simeq B)}$

co wyraża, że ​​typy, które są równe, są w szczególności również równoważne. ${\ Displaystyle A, B}$

Univalence aksjomat stwierdza, że funkcja ta sama jest równoważność. Dlatego mamy

${\ Displaystyle (A = B) \ Simeq (A \ Simeq B)}$

„Innymi słowy, tożsamość jest równoznaczna z równoważnością. W szczególności można powiedzieć, że »typy równoważne są identyczne«”.

Aplikacje

Dowodzenie twierdzenia

HoTT pozwala na znacznie łatwiejsze niż dotychczas tłumaczenie dowodów matematycznych na język programowania komputerowego dla asystentów komputerowych . Takie podejście daje komputerom możliwość sprawdzenia trudnych dowodów.

Jednym z celów matematyki jest sformułowanie aksjomatów, z których można wyprowadzić i jednoznacznie udowodnić praktycznie wszystkie twierdzenia matematyczne. Poprawne dowody w matematyce muszą być zgodne z zasadami logiki. Muszą być bezbłędnie wyprowadzane z aksjomatów i już sprawdzonych stwierdzeń.

HoTT dodaje aksjomat jednowartościowości, który wiąże równość twierdzeń logiczno-matematycznych z teorią homotopii. Równanie takie jak „a=b” to zdanie matematyczne, w którym dwa różne symbole mają tę samą wartość. W teorii typów homotopii oznacza to, że dwa kształty reprezentujące wartości symboli są topologicznie równoważne.

Te topologiczne relacje równoważności, jak twierdzi dyrektor Instytutu Badań Teoretycznych ETH Zürich Giovanni Felder , można lepiej sformułować w teorii homotopii, ponieważ jest ona bardziej wszechstronna: teoria homotopii wyjaśnia nie tylko, dlaczego „a równa się b”, ale także jak to wyprowadzić. W teorii mnogości te informacje musiałyby być dodatkowo zdefiniowane, co utrudnia tłumaczenie zdań matematycznych na języki programowania.

Programowanie komputerowe

Od 2015 r. trwały intensywne prace badawcze nad modelowaniem i formalną analizą obliczeniowego zachowania aksjomatu jednowartościowości w teorii typu homotopii.

Teoria typów sześciennych jest jedną z prób nadania zawartości obliczeniowej teorii typów homotopii.

Uważa się jednak, że pewne obiekty, takie jak typy semi-simplicial, nie mogą być konstruowane bez odniesienia do jakiegoś pojęcia dokładnej równości. W związku z tym opracowano różne dwupoziomowe teorie typów, które dzielą ich typy na typy fibrantowe, które respektują ścieżki, i typy niefibrantowe, które nie. Kartezjańska sześcienna teoria typów obliczeniowych jest pierwszą dwupoziomową teorią typów, która daje pełną interpretację obliczeniową teorii typów homotopii.

Zobacz też

• Rachunek konstrukcji
• Korespondencja Curry-Howard
• Teoria typów intuicjonistycznych
• Hipoteza homotopii
• Fundamenty jednowartościowe

Bibliografia

Bibliografia

Dalsza lektura

• David Corfield (2020), Modalna teoria typów homotopii: perspektywa nowej logiki dla filozofii , Oxford University Press.

Linki zewnętrzne

• Teoria typów homotopii
• Teoria typów homotopii w nLab
• Wiki o teorii typów homotopii
• Strona internetowa Władimira Wojewodskiego na temat Fundacji Uniwalentnych
• Teoria typów homotopii i jednowartościowe podstawy matematyki Steve Awodey
• „Konstruktywna teoria typów i homotopia” – wykład wideo Steve'a Awodeya w Institute for Advanced Study

Biblioteki matematyki sformalizowanej