Парадокс Рассела: реализация на Агде

[deni_ok]

К вопросу о заселении ⊥ при включенном type-in-type. Делается прямой реализацией парадокса Рассела

{-# OPTIONS --type-in-type --without-K

Comments

[voidex]

Ещё тут есть:

https://gist.github.com/copumpkin/2631136

[deni_ok]

Да, уже приближается к статусу фольклора.

[sassa_nf]

а в каком смысле "invert" что-то инвертирует?

[voidex]

Подозреваю что "инвертирует" f, для x и f возвращает y такой, что f y ≡ x

[nivanych]

Есличо - я только говорил, что есть импредикативные непротиворечивые системы ;-)
Элементарные топосы, например.

[deni_ok]

не, я помню, именно так и говорил :)

[nivanych]

;-) Не буду искать пруфлинк.

[deni_ok]

Я имел ввиду, что ты говорил именно так, как и написал в своем предыдущем комменте. Нечётко формулирую спросонья, сорри.