Many Faces of Univalence

На прошлом уроке мы познакомились с расслоениями пространств, как ближайшими изоморфизмами для пи и сигма типов. В MLTT вообще много изоморфизмов, поэтому, когда дают определение чему-то, всегда говорят up to isomorphism, именно так родилось определение Категории в учебнике HoTT, с помощью пополнения Rezk. В нашей базовой библиотеке именно такое определение. У равенства в MLTT есть три изоморфизма которые учавствуют в описании унивалентности: 1) это встроенный в тайпчекер Path, 2) это эквивалентность которая определяется через расслоения и 3) изоморфизм который опрделеяется как пара морфизмов A -> B, B -> A, левая и правая композиция которых это тождественная функция А или B типа. Так вот iso уже посложнее выглядит как терм, а эквивалентность еще не такая сложная. Всего при трех равенствах получается 18 унивалентных теорем о равенствах: Iso(Path,Equiv), Equiv(Path,Iso), ...т.е. флипы аргументов, в разные стороны стрелки, и в разном порядке все равенства.

[1]. M.Sokhatskyi. Addendum II: Many Faces of Equality