L
Полезная инфа
Size: a a a
2021 April 10
KR
Какие это измерения?
p
Значения, типы и типы типов
И все может зависеть друг от друга
И все может зависеть друг от друга
H
пошёл направа завтипов хапнул, пошёл налево -- HKT и т.д.
H
в самом верху CoC -- calculus of constructions
KR
Так понятно, спасибо
L
Это как на уроках химии, училка говорит решите задачи с магнием и кальцием , в жизни это вам очень нужно будет, но в итоге я даже в глаза магний и кальций никогда не видел и врядли увижу
H
cock
L
Дата саинс это разве не околопрограммисткое направление?
AN
не надо тут сравнивать великую прикладную науку с дрочем на типчики
H
ещё есть обобщение лямбда куба -- чистые системы типов. это считай тензоры. но зачем надо хщ
KR
Оно ведь universes называется? Или то другое?
AN
*ЗЫ cообщите если слишком толсто набрасываю
H
скорее иерархия сортов
p
Это про типы типов типов типов типов
KR
Как Arend? Для пруверов?
H
universes хотя да, просто не помню уже
AN
TK
Зочим
L
Химия великая наука? Не отрицаю, но не в системе образования СНГ она великая