C1 Категория

Категория — это

* Типы Ob, Mor
* Функции dom, cod, ∘, id
* Естественные равенства на них (конечно, связанные естественными равенствами следующего уровня and so on to ∞)
* Унивалентность: id: Ob -> Isom является изоморфизмом типов (где Isom, конечно, подтип в Mor, морфизмов, для которых просто существует обратный)

(как видно, неточность здесь только 3-ем компоненте, с точным выражением которого текущие варианты HoTT собственно пока не могут справиться. Но которое легко формулируется, если добавить в язык дискретный слой, из которого собственно целиком и состоят традиционные теоретико-множественные основания, где мы умеем определять все что хотим, ценой пропасти между формальным текстом и представляемой им содержательной математикой)

Так, например, старое/традиционное понятие категории — это частный случай, который следует называть 1-усеченные категории т.е. такие, что в них все Hom(A, B) = {f : Mor | dom f = A, cod f = B}} являются множествами (0-типами). В этом случае понятно, что все старшие равенства тривиализуются и просто традиционные аксиомы категории на операции, пополненные унивалентностью, в этом случае дают полное правильное определение.

Унивалентность гласит: изоморфизмы объектов то же самое, что их равенства (то есть, все изоморфизмы объектов приходят из равенств между объектами, равенства между изоморфизмами из равенств между равенствами и т.д.). То есть фактор-тип от Ob, возникающий из структуры категории — тривиальный, он совпадает с исходным Ob (а мог быть вообще говоря более грубым, стрелка могла быть некоторой сюръекцией типов Ob -> Ob_cat).

Так, например, в случае классических категорий, таких как Set, Group, Top, аксиома форсирует, что их типы объектов — изначально являются группоидами (группоидами изоморфизмов в соотв. категории), а не множествами, как это привычно в представлении категорий в языке множеств (с множествами объектов стрелка как раз будет нетривиальной сюръекцией, фейля унивалентность, а все остальные аксиомы категории будут выполнены).

Как и можно было почувствовать из естественности аксиомы, оказывается, что, с такой настройкой (зафиксировав так на уровне определения категории принцип структурализма, обсуждавшийся выше) теория категория становится совершенной. Часть списка свидетельств её естественности можно найти по этим nlab-ссылкам homotopy type theory, anafunctor.

И кроме того, в точности это понятие и было определено, во всех этих эквивалентных определениях (∞, 1)-категорий, а одно из них (которое я, кстати, нахожу наиболее естественным, удобным и интуитивным — в терминах полных пространств Сигала), содержит буквально аксиому унивалентности непосредственно. Только Резк, опубликовавший это понятие в 1998 году, за 10 лет до Воеводского, дал ей неприметное имя «полнота».