Это замечательный пост. Я как раз в депендент тайпах повис где-то вокруг понимания A → ⊥, так что, для меня очень вовремя :)


Я бы irrefutable переводил как "неопровержимость"

Про замену классических конструктивными понятно, хотя и не прочувствовал.


"Наконец, irrefutable оно, когда его отрицание ложно."

здесь "оно" относится к "истинно" или "ложно"? Или в смысле, что не важно, вычислимо ли, главное, что отрицание ложно?