![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Новости HoTT
Apr. 17th, 2016 12:05 amНа днях Altenkirch, Capriotti и Kraus (arxiv:1604.03799) выложили препринт о технике расширения HoTT предтипами (соответствующими в моделях нефибрантным объектам), и в особенности предтипом строгого равенства. Получившаяся теория типов имеет разрешимый тайпчекинг, и, судя по всему (доказательство разных тонких обещают скоро опубликовать в рамках диссертации Каприотти) является консервативным над HoTT. С одной стороны, так теряется одно из основных преимуществ HoTT — априорная non-evelness, т.е. “all grammatically correct properties of objects are invariant under isomorphism”. А в расширенной HoTT существуют “предсвойства”, которые вдоль изоморфизма не переносятся.
Зачем это расширение нужно? — для того, чтобы можно было определять структуры со строгим равенством, в особенности инфинитарные структуры вроде слабых (∞,1)-категорий так, как это делается в математике сейчас. С одной стороны, я не теряю надежды, что можно определить такие объекты и в полностью фибрантном расширении HoTT (включающем, однако, высшие коиндуктивные типы, чтобы можно было определить ∞-категории пользуясь подходом из “Weak ω-categories via terminal coalgebras“ Eugenia Cheng, Tom Leinster), с другой стороны расширение Альтенкирха сотоварищи нужно уже затем, чтобы отражать имеющиеся практики в математике, ну и главное, этот подход работает прямо сейчас, а не когда-нибудь, когда рак на горе свиснет и придумается правильное фибрантное расширение.
Вообще, я не верю в то, что judgemental equality в теории типов имеет семантический смысл, в частности потому что при определении теорий типов без суждений вида a ≡ b вполне можно обойтись, если использовать подход с двусторонним тайпчекингом (bi-directional typechecking), который на практике выглядит гораздо более естественным. Разумеется, задание всех правил двустороннего тайпчекинга даёт отношение “a можно подставить вместо b” на термах, и если два терма можно подставлять друг вместо друга в обе стороны, то их логично называть подстановочно равными. Однако это выглядит скорее как свойство термов, а не как свойство объектов, ими обозначаемых.
Зачем это расширение нужно? — для того, чтобы можно было определять структуры со строгим равенством, в особенности инфинитарные структуры вроде слабых (∞,1)-категорий так, как это делается в математике сейчас. С одной стороны, я не теряю надежды, что можно определить такие объекты и в полностью фибрантном расширении HoTT (включающем, однако, высшие коиндуктивные типы, чтобы можно было определить ∞-категории пользуясь подходом из “Weak ω-categories via terminal coalgebras“ Eugenia Cheng, Tom Leinster), с другой стороны расширение Альтенкирха сотоварищи нужно уже затем, чтобы отражать имеющиеся практики в математике, ну и главное, этот подход работает прямо сейчас, а не когда-нибудь, когда рак на горе свиснет и придумается правильное фибрантное расширение.
Вообще, я не верю в то, что judgemental equality в теории типов имеет семантический смысл, в частности потому что при определении теорий типов без суждений вида a ≡ b вполне можно обойтись, если использовать подход с двусторонним тайпчекингом (bi-directional typechecking), который на практике выглядит гораздо более естественным. Разумеется, задание всех правил двустороннего тайпчекинга даёт отношение “a можно подставить вместо b” на термах, и если два терма можно подставлять друг вместо друга в обе стороны, то их логично называть подстановочно равными. Однако это выглядит скорее как свойство термов, а не как свойство объектов, ими обозначаемых.
