AK
ID:402926333
Я так понимаю что унивалентность нам нагадила и стираемость пропсов пропала (т.е. может что-то и можно стереть но нет понимания что можно а что низя)
Нет, не унивалентность, а само существование Id-типов, не являющихся пропозишнами.
Size: a a a
2017 November 21
NK
т.е. нарушение UIP
TN
наличие гомотопического отрезка, лямбды на нем, и апликации — компонентов Id
AK
Да. Причём даже если вы без унивалентности и высших гомотопических типов просто хотите, чтобы у вас была функциональная экзистенциональность и фактортипы, то стирать просто так уже нельзя.
AK
Стирается вычислительно-релевантная информация.
AG
а в OTT как тогда выкручивались?
AK
а в OTT как тогда выкручивались?
Там не было фактортипов. И это вообще основная беда там была.
NK
Стирается вычислительно-релевантная информация.
О чём я и говорю, что мы не можем ограничить себя так, чтобы было понятно что нерелевантно. Или можем?
AG
это которые quotient types?
AK
а в OTT как тогда выкручивались?
Уж они и так пытались, и сяк, но не выходил каменный цветок. И только после HoTT стало понятно, что не выходил ровно потому, что не мог выйти. Да, это которые Quotient Types. Или, более конкретно — Quotient Inductive Types.
AK
Т.е. типы, которые определяются как высшие гомотопические, но при этом имеют Prop-like равенство.
NK
так более понятно
AK
Как бы так сделать, чтобы было понятно, что релевантно, а что нет, вроде недавно придумал МакБрайд.
TN
я ксати как-то сразу сообразил, что инвестировать во всякие JM_Eq и OTT нет смысла :-)
AK
Информация от Хенкока. От макбрайда информации нет ни в каком виде. Ни видео, ни заметок, ни черновика.
NK
Но у него же нет равенства, следующего из изоморфизма? Мне кажется мы достаточно долго можем жить с такой ослабленной унивалентностью
AK
ID:402926333
Но у него же нет равенства, следующего из изоморфизма? Мне кажется мы достаточно долго можем жить с такой ослабленной унивалентностью
У кого?
NK
у макбрайда
AK
Я ничего не знаю, про то что придумал макбрайд. Видимо, оно либо не работает, либо бомба, которую он усиленно готовит к публикации.
NK
ага