Скажем, я работаю в теории гомотопического типа, и мои единственные объекты изучения - это условные категории.
Эквивалентности здесь даны функторами а также которые обеспечивают эквивалентность категорий , Существуют природные изоморфизмы а также так что этот функтор и «обратный» функтор преобразуются в функтор единиц.
Теперь однолистность связывает эквивалентности с типом идентичностииз теории преднамеренного типа я выбрал говорить о категориях. Поскольку я имею дело только с категориями, и они эквивалентны, если у них есть изоморфные скелеты , мне интересно, могу ли я выразить аксиому однолистности в терминах перехода к скелету категорий.
Или, в противном случае, я могу определить тип идентичности, то есть синтаксическое выражение таким образом, что по существу говорит «есть скелет (или isomorphi) и а также оба эквивалентны этому. "?
(Выше я пытаюсь интерпретировать теорию типов в терминах понятий, которые легче определить, - теоретических понятий категории. Я думаю об этом, потому что с моральной точки зрения мне кажется, что аксиома «исправляет» теорию преднамеренного типа жестким кодированием принцип эквивалентности , который уже является естественной частью формулировки категории теоретических утверждений, например , задающими объекты только в терминах универсальных свойств.)
Ответы:
Я отсылаю вас к главе 9 книги HoTT. В частности, категория определяется таким образом, чтобы изоморфные объекты были равны, см. Определение 9.1.6 . Как показано в примере 9.1.15 , в HoTT действительно нет разумного понятия «скелетность». Это так, потому что равенство настолько слабо, что оно уже означает «изоморфный».
Кроме того, теорема 9.4.16 говорит
Теорема говорит нам, что аксиома однолистности дает нам своего рода мечту теоретика катетеризации: эквивалентные категории равны.
Вы спрашиваете, можете ли вы свести аксиому об однозначности к утверждению о категориях. Попытки использовать скелеты не будут работать, потому что нет хорошего способа сказать «скелет». Мы могли бы спросить, подразумевает ли теорема 9.4.16 аксиому однолистности. Насколько я понимаю, этого не произойдет, потому что категория имеет1 тип (группоид) объектов и 0 -тип (набор) морфизмов, поэтому теорема 9.4.16 представляет собой нечто вроде аксиомы однолистности только для 1-типов.
источник