Отношение однолистности для теории категрий к концепции скелета

10

Скажем, я работаю в теории гомотопического типа, и мои единственные объекты изучения - это условные категории.

Эквивалентности здесь даны функторами F:DC а также G:CDкоторые обеспечивают эквивалентность категорий CD, Существуют природные изоморфизмыα:nat(FG,1C) а также β:nat(GF,1D) так что этот функтор и «обратный» функтор преобразуются в функтор единиц.

Теперь однолистность связывает эквивалентности с типом идентичностиC=Dиз теории преднамеренного типа я выбрал говорить о категориях. Поскольку я имею дело только с категориями, и они эквивалентны, если у них есть изоморфные скелеты , мне интересно, могу ли я выразить аксиому однолистности в терминах перехода к скелету категорий.

Или, в противном случае, я могу определить тип идентичности, то есть синтаксическое выражение C=D:= таким образом, что по существу говорит «есть скелет (или isomorphi) и C а также D оба эквивалентны этому. "?

(Выше я пытаюсь интерпретировать теорию типов в терминах понятий, которые легче определить, - теоретических понятий категории. Я думаю об этом, потому что с моральной точки зрения мне кажется, что аксиома «исправляет» теорию преднамеренного типа жестким кодированием принцип эквивалентности , который уже является естественной частью формулировки категории теоретических утверждений, например , задающими объекты только в терминах универсальных свойств.)

Nikolaj-K
источник
2
Вы читали главу 9 книги HoTT? Это о теории категорий.
Андрей Бауэр

Ответы:

11

Я отсылаю вас к главе 9 книги HoTT. В частности, категория определяется таким образом, чтобы изоморфные объекты были равны, см. Определение 9.1.6 . Как показано в примере 9.1.15 , в HoTT действительно нет разумного понятия «скелетность». Это так, потому что равенство настолько слабо, что оно уже означает «изоморфный».

Кроме того, теорема 9.4.16 говорит

Теорема 9.4.16: еслиA а также B категории, то функция

(A=B)(AB)
(определяется индукцией по тождественному функтору) - это эквивалентность типов.

Теорема говорит нам, что аксиома однолистности дает нам своего рода мечту теоретика катетеризации: эквивалентные категории равны.

Вы спрашиваете, можете ли вы свести аксиому об однозначности к утверждению о категориях. Попытки использовать скелеты не будут работать, потому что нет хорошего способа сказать «скелет». Мы могли бы спросить, подразумевает ли теорема 9.4.16 аксиому однолистности. Насколько я понимаю, этого не произойдет, потому что категория имеет1тип (группоид) объектов и 0-тип (набор) морфизмов, поэтому теорема 9.4.16 представляет собой нечто вроде аксиомы однолистности только для 1-типов.

Андрей Бауэр
источник