s
Ну а что ты хотел? HoTT это не про спецэффекты.
Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
505 membersпожаловаться на группу
2021 November 23
s
Вертолёты не взрывает, слоумо не делает.
NR
Ну вот мне и интересно про что. Чтоб не просто переопределить всё ещё раз а чтоб что нибудь получилось из этого
NR
Если что для меня "глянь какая изящная хрень получилась" это аргумент
MT
Всё мечтаю срастить ХоТТ и ТК. И, наверное, это уже кто-то сделал. Но я не могу поднять...
AC
Как известно, HoTT относится к так называемым "основаниям математики", а эти самые основания занимаются "пониманием" (или описанием) тривиальных фундаментальных понятий. Это по определению не впечатляет, потому что все думают, что понимают, пока не начнут закапываться в то, что же это такое на самом деле.
NR
Да, я так себе это и представлял. Вот хочу как раз какой нибудь показательный пример конфуза который хотт разрешает.
AC
Так категории кубов же, нет?
s
Из более впечатляющего: возможность определить мультимножество как индуктивный тип.
AC
Про
-0 = +0 уже было. В целом, можно сказать, что HoTT и унивалентность — это про равенство: что чему равно когда и почему.NR
О. Это звучит как что-то в чем можно разобраться.
NR
Может и готовая ссылка есть которая покажет всю магию?
AC
А что там с quotients? 😂
NR
А тут совсем не понятно к сожалению.
MT
Уважаемый Александр! Не соблаговолите ли ткнуть носом, пожалуйста?
NR
Ну где была проблема и в чем решение.
NR
На канале Topos institute были лекции
AC
Да я сам только краем уха слышал, но могу поискать. На nCatLab. 😁
AC
А как Вы определяете целые числа? Желательно, в виде индуктивного типа? 😊