AG
в ванильном хотте их нет
Size: a a a
2020 December 04
AG
точнее его можно определить уже внутри самой теории
AG
но волшебного статуса у него нет
DB
а точно не нужно сначала вкатиться в Теворею Группп?
к
ну под интервалом [0..1] я имел виду топологический интервал для гомотопий
AG
а точно не нужно сначала вкатиться в Теворею Группп?
неплохо бы, потому что именно в группах появляется мотивация городить все эти факторы и изоморфизмы
к
правда там тоже не [0..1]
к
а сфера н-мерная для н-ой готопии
к
почти как в аренде
к
а хм
к
я понял тогда почему в аренде так
AG
как?
R
да кубы надо просто изучать в отрыве от хотта. "Как сделать систему, в которая funext доказуема?" — "А вот так, например"
AG
для фунэкста не надо городить хомотопии
AG
достаточно ott/sett
R
и не надо морочиться с этой всей унивалентностью
VD
Я вот иногда читаю этот чат и наверное чувствую себя как мои коллеги в чате, когда я им про хасскел рассказываю
R
достаточно ott/sett
поэтому там "например"
VD
Чому до этого никто матаны в языки не пытался тащить?
AG
до какого этого?