мини|Насловна страна књиге Homotopy Type Theory: Univalent Foundations of Mathematics. У математичкој логици и рачунарству, хомотопска теорија типова (HoTT) обухвата различите правце развоја интуиционистичке теорије типова, засноване на интерпретацији типова као објеката на које се примењује интуиција (апстрактне) хомотопске теорије.
Ово укључује, између осталог, конструкцију хомотопских и вишекатегоричких (енгл. higher-categorical) модела за овакве теорије типова; употребу теорије типова као логике (или унутрашњег језика) за апстрактну хомотопску теорију и теорију виших категорија; развој математике унутар теоретско-типских основа (укључујући како претходно постојећу математику, тако и нову математику коју хомотопски типови омогућавају); као и формализацију сваког од ових праваца у рачунарским доказивачима теорема.
Постоји велико преклапање између рада који се назива хомотопска теорија типова и пројекта познатог као унивалентне основе. Иако ниједан није прецизно разграничен, а термини се понекад користе као синоними, избор употребе понекад одговара разликама у гледишту и нагласку., фуснота 1 Због тога, овај чланак можда не представља једнако ставове свих истраживача у овим областима. Оваква варијабилност је неизбежна када је област у брзом развоју.
Историја
Групоидни модел У једно време, идеја да се типови у интензионалној теорији типова са својим типовима идентитета могу сматрати групоидима била је део математичког фолклора. То је први пут семантички прецизирано у раду Мартина Хофмана (Martin Hofmann) и Томаса Штрајхера (Thomas Streicher) из 1994. године под називом „The groupoid model refutes uniqueness of identity proofs”, у којем су показали да интензионална теорија типова има модел у категорији групоида. Ово је био први истински „хомотопски” модел теорије типова, иако само „1-димензионалан” (будући да су традиционални модели у категорији скупова хомотопски 0-димензионални).
Њихов наредни рад наговестио је неколико каснијих достигнућа у хомотопској теорији типова. На пример, приметили су да групоидни модел задовољава правило које су назвали „екстензионалност универзума”, што није ништа друго до ограничење на 1-типове аксиоме униваленције коју је Владимир Војеводски предложио 10 година касније. (Међутим, аксиому за 1-типове је знатно једноставније формулисати, јер није потребан кохерентан појам „еквиваленције”.) Такође су дефинисали „категорије са изоморфизмом као једнакошћу” и поставили хипотезу да би се у моделу који користи вишедимензионалне групоиде, за такве категорије важило „еквиваленција је једнакост”; ово су касније доказали Бенедикт Аренс (Benedikt Ahrens), Кшиштоф Капулкин (Krzysztof Kapulkin) и Мајкл Шулман (Michael Shulman).
Рана историја: категорије модела и виши групоиди Прве вишедимензионалне моделе интензионалне теорије типова конструисали су Стив Аводи и његов студент Мајкл Ворен (Michael Warren) 2005. године користећи Квиленове категорије модела. Ови резултати су први пут јавно представљени на конференцији FMCS 2006, на којој је Ворен одржао предавање под насловом „Homotopy models of intensional type theory”, што је уједно послужило као проспект његове тезе (присутна комисија за дисертацију били су Аводи, Никола Гамбино и Алекс Симпсон). Сажетак се налази у апстракту Вореновог проспекта тезе.
На накнадној радионици о типовима идентитета на Универзитету у Упсали 2006. године, одржана су два предавања о односу између интензионалне теорије типова и система факторизације: једно које је одржао Ричард Гарнер (Richard Garner), „Factorisation systems for type theory”,Richard Garner, Factorisation axioms for type theory и једно које је одржао Мајкл Ворен, „Model categories and intensional identity types”. Сродне идеје су разматране у предавањима Стива Аводија, „Type theory of higher-dimensional categories”, и Томаса Штрајхера, „Identity types vs. weak omega-groupoids: some ideas, some problems”. На истој конференцији Бено ван ден Берг (Benno van den Berg) одржао је предавање под насловом „Types as weak omega-categories” где је изложио идеје које су касније постале предмет заједничког рада са Ричардом Гарнером.
Све ране конструкције вишедимензионалних модела морале су да се суоче са проблемом кохерентности типичним за моделе зависне теорије типова, те су развијена различита решења. Једно такво решење је дао Војеводски 2009. године, а друго ван ден Берг и Гарнер 2010. године. Опште решење, засновано на конструкцији Војеводског, на крају су дали Ламсдејн (Peter LeFanu Lumsdaine) и Ворен 2014. године.
На семинару PSSL86 2007. године, Аводи је одржао предавање под називом „Homotopy type theory” (ово је била прва јавна употреба тог термина, који је сковао сам АводиPreliminary list of PSSL86 participants). Аводи и Ворен су сажели своје резултате у раду „Homotopy theoretic models of identity types”, који је објављен на серверу за препринте ArXiv 2007. године, а званично издат 2009. године; детаљнија верзија се појавила у Вореновој тези „Homotopy theoretic aspects of constructive type theory” 2008. године.
Отприлике у исто време, Владимир Војеводски је независно истраживао теорију типова у контексту потраге за језиком за практичну формализацију математике. У септембру 2006. послао је мејлинг листи „Types” поруку „A very short note on homotopy lambda calculus”, која је скицирала обрисе теорије типова са зависним производима, сумама и универзумима, као и модела ове теорије типова у Кановим симплексним скуповима. Започела је речима „Хомотопски λ-рачун је хипотетички (у овом тренутку) систем типова” и завршила са „У овом тренутку већи део онога што сам горе рекао је на нивоу хипотеза. Чак је и дефиниција модела TS-а у хомотопској категорији нетривијална”, односећи се на сложена питања кохерентности која нису била решена све до 2009. године. Ова белешка је укључивала синтаксичку дефиницију „типова једнакости” за које се тврдило да се у моделу тумаче просторима путева, али није узимала у обзир правила Пера Мартин-Лефа за типове идентитета. Такође је стратификовала универзуме по хомотопској димензији поред величине, што је идеја која је касније углавном одбачена.
Са синтаксичке стране, Бено ван ден Берг је 2006. године поставио хипотезу да кула типова идентитета неког типа у интензионалној теорији типова треба да има структуру ω-категорије, и штавише ω-групоида, у „глобуларном, алгебарском” смислу Мајкла Батанина (Michael Batanin). Ово су касније независно доказали ван ден Берг и Гарнер у раду „Types are weak omega-groupoids” (објављен 2008), као и Питер Ламсдејн у раду „Weak ω-Categories from Intensional Type Theory” (објављен 2009) и као део његове докторске дисертације из 2010. године „Higher Categories from Type Theories”.
Аксиома униваленције, синтетичка хомотопска теорија и виши индуктивни типови Концепт унивалентне фибрације увео је Војеводски почетком 2006. године.Notes on homotopy lambda calculus, March 2006 Међутим, због инсистирања свих презентација Мартин-Лефове теорије типова на својству да типови идентитета, у празном контексту, могу садржати само рефлексивност, Војеводски све до 2009. није препознао да се ови типови идентитета могу користити у комбинацији са унивалентним универзумима. Конкретно, идеја да се униваленција може увести једноставним додавањем аксиоме постојећој Мартин-Лефовој теорији типова појавила се тек 2009. године.
Такође у 2009. години, Војеводски је разрадио више детаља модела теорије типова у Кановим комплексима, и приметио да се постојање универзалне Канове фибрације може искористити за решавање проблема кохерентности за категоричке моделе теорије типова. Такође је доказао, користећи идеју А. К. Баусфилда (A. K. Bousfield), да је ова универзална фибрација унивалентна: придружена фибрација хомотопских еквиваленција у паровима између влакана је еквивалентна фибрацији простора путева базе.
Да би формулисао униваленцију као аксиому, Војеводски је пронашао начин да синтаксички дефинише „еквиваленције”, које су имале важно својство да је тип који представља тврдњу „f је еквиваленција” био (под претпоставком екстензионалности функције) (-1)-скраћен (тј. контрактибилан ако је настањен). Ово му је омогућило да дâ синтаксичку тврдњу о униваленцији, уопштавајући Хофманову и Штрајхерову „екстензионалност универзума” на више димензије. Такође је био у стању да искористи ове дефиниције еквиваленција и контрактибилности да започне развој значајних количина „синтетичке хомотопске теорије” у доказивачу теорема Rocq (раније познатом као Coq); ово је формирало основу библиотеке која је касније названа „Foundations”, а на крају „UniMath”.GitHub repository, Univalent Mathematics
Уједињење различитих токова почело је у фебруару 2010. године неформалним састанком на Универзитети Карнеги Мелон, где је Војеводски представио свој модел у Кановим комплексима, и своју верзију Rocq-а, групи која је укључивала Аводија, Ворена, Ламсдејна, Роберта Харпера, Дена Ликату, Мајкла Шулмана и друге. Овај састанак је резултирао нацртима доказа (чији су аутори Ворен, Ламсдејн, Ликата и Шулман) да је свака хомотопска еквиваленција заправо еквиваленција (у добром кохерентном смислу Војеводског), на основу идеје из теорије категорија о побољшању еквиваленција до адјунгованих еквиваленција. Убрзо након тога, Војеводски је доказао да аксиома униваленције имплицира екстензионалност функције.
Следећи кључни догађај била је мини-радионица на Математичком истраживачком институту у Оберволфаху у марту 2011. коју су организовали Стив Аводи, Ричард Гарнер, Пер Мартин-Леф и Владимир Војеводски, под називом „The homotopy interpretation of constructive type theory”. Као део Coq туторијала за ову радионицу, Андреј Бауер (Andrej Bauer) је написао малу Coq библиотекуGitHub repository, Andrej Bauer, Homotopy theory in Coq засновану на идејама Војеводског (али заправо не користећи ниједан његов код); ово је на крају постало језгро прве верзије Coq библиотеке „HoTT” (први комит ове друге библиотекеGitHub repository, Homotopy type theory од стране Мајкла Шулмана напомиње „Развој заснован на датотекама Андреја Бауера, са многим идејама преузетим из датотека Владимира Војеводског”). Једна од најважнијих ствари произашлих из састанка у Оберволфаху била је основна идеја виших индуктивних типова, заслугом Ламсдејна, Шулмана, Бауера и Ворена. Учесници су такође формулисали листу важних отворених питања, као што су да ли аксиома униваленције задовољава каноничност (још увек отворено, иако су неки специјални случајеви позитивно решени), да ли аксиома униваленције има нестандардне моделе (од тада позитивно одговорено од стране Шулмана), и како дефинисати (полу)симплексне типове (још увек отворено у MLTT, иако се може урадити у Хомотопском систему типова (HTS) Војеводског, теорији типова са два типа једнакости).
Убрзо након радионице у Оберволфаху, покренути су веб-сајт и блог хомотопске теорије типова,Homotopy Type Theory and Univalent Foundations Blog и тема је почела да се популаризује под тим именом. Увид у неке од важних напредака током овог периода може се добити из историје блога.Homotopy Type Theory blog
Унивалентне основе Израз „унивалентне основе” сви сматрају уско повезаним са хомотопском теоријом типова, али га не користе сви на исти начин. Првобитно га је користио Владимир Војеводски како би означио своју визију основног система за математику у којем су основни објекти хомотопски типови, засновани на теорији типова која задовољава § аксиому униваленције, и формализовани у рачунарском доказивачу теорема.Type Theory and Univalent Foundations