VZ
Coq
Size: a a a
2020 July 03
MK
а пример не такой?
VZ
Cubical Agda насколько я понимаю, @effectfully может меня поправить
MK
спасибо
MK
а обычная агда нет?
VZ
По идее да, но у них тоже есть какое-то свое понятие relevance, в котором я до конца не разобрался, и не знаю, как оно со всем этим связано
VZ
Надо полагать, что если там можно явно пометить инпут как нерелевантный, то по умолчанию что-то релевантное происходит
VZ
Ок, похоже я про Coq тоже не совсем прав – там тоже не гарантируется proof irrelevance
MK
посмотрел доклад про ATS который тут кидали, прикольно
MK
я почему-то думал что это изотерика уровня J, но вроде нет
VZ
пример такой системы?
Похоже Lean
VZ
а пример не такой?
Похоже тоже Lean (в HoTT mode)
MK
прикольно
DI
https://www.youtube.com/watch?v=KokvdcF0t2U примерно через 1:50:00 от начала
2020 July 04
DI
а нет, 1:10:00
DI
видимо, там с перерывами
DI
и какой-то левый гражданин в углу