к
в лине кстати if и работает с decidable утверждениями, а не слепыми булами, но даже в нем он не пробрасывает их в контекст
Size: a a a
2020 December 04
AG
не обязательно
а где доживают?
AG
я про пруфы именно равенства
к
в кубиках же доживать должно
AG
а чо у кубиков уже рантайм есть?
DB
Чо за кубеки
к
ну ладно, возможно в принципе с хоттом доживать должно
к
у аренда есть рантайм?
к
ну вроде нет, ладно
AA
если могут не доживать не значит же что не будут
к
вот почему
к
там же if явно с decidable работает, то есть ну он уже точно знает что все есть
AG
Чо за кубеки
модель гомотопической теории типов в кубических множествах
DB
модель гомотопической теории типов в кубических множествах
Звучит как мем. Лямбда куб еще понимаю, этого не понимаю
AG
это на пару шагов дальше лямбда куба
AG
здесь правда только часть возможностей используется
DB
non-empty list is equal to its tail.
DB
Это как
к
ну просто вот так