Когда мы смотрим на книгу «Гомотопическая теория типов» - мы видим следующие темы:
Homotopy type theory
2.1 Types are higher groupoids
2.2 Functions are functors
2.3 Type families are fibrations
2.4 Homotopies and equivalences
2.5 The higher groupoid structure of type formers
2.6 Cartesian product types
2.7 S-types
2.8 The unit type
2.9 P-types and the function extensionality axiom
2.10 Universes and the univalence axiom
2.11 Identity type
2.12 Coproducts
2.13 Natural numbers
2.14 Example: equality of structures
2.15 Universal properties
Теперь мы знаем, что не вся теория гомотопического типа возможна - это Agda и Coq .
Мой вопрос: какие части теории гомотопического типа невозможны в Agda или Coq?
type-systems
Hawkeye
источник
источник
Ответы:
Если вы посмотрите на Заметки о главе 8 вы увидите , что уже уже формализованы, и я думаю , что это очень много. Есть библиотека Coq HoTT и библиотека Agda HoTT-Agda, которые формализуют большие куски теории гомотопического типа.
Чтобы добиться успеха в Coq, нам нужна была специальная версия Coq, которая была исправлена только для целей HoTT. Однако Coq движется в направлении поддержки теории гомотопического типа, поэтому вскоре мы сможем сделать это с помощью стандартного Coq.
В Agda нужно включить
--without-Kопцию, иначе Agda считает, что все типы являются 0-типами. Есть некоторые затянувшиеся сомнения относительно того,--without-Kдействительно ли избавляется от предположения, что все является 0-множеством, или, возможно, можно было бы повторно ввести его в Agda с хитрым использованием сопоставлений с образцом.Следующие аспекты формализации Coq и Agda не являются удовлетворительными:
Аксиома однолистности сформулирована как гипотеза. Было бы лучше, если бы он был встроен в систему. В частности, мы бы хотели, чтобы Coq и Agda поняли правила вычисления аксиомы однолистности.
Аналогично, мы должны использовать хаки, чтобы получить работоспособные типы с более высокой индуктивностью. Опять же, было бы лучше иметь прямую поддержку.
Проблема с вышеуказанными недостатками состоит в том, что никто не знает, как их исправить, даже теоретически. Это активная область исследований.
Кроме того, я думаю , что это справедливо сказать , что HOTT может быть в основном сделано в Coq и Agda, просто не оптимальным образом.
источник
ua, константа, которая свидетельствует об аксиоме однолистности? Каковы правила вычисления для HIT? У нас есть некоторые идеи, но ничего водонепроницаемого.Насколько я понимаю, в Agda можно представить все это (т. Е. Всю главу 2 - на github есть библиотека, которая делает; AFAIK, то же самое верно и для Coq). Только когда вы переходите к последующим главам, все становится рискованно. Есть два очевидных момента:
Есть и другие пункты, но я еще не дошел до прочтения этой части формализации Agda ... Но в целом большая часть HoTT может быть хорошо формализована как в Agda, так и в Coq.
Что еще более важно, обе команды разработчиков активно работают над адаптацией своих систем, чтобы можно было обрабатывать больше HoTT, по крайней мере, когда есть четкая теория о том, как реализовать необходимые функции. Это оказалось сложным по частям.
источник