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

[deni_ok]

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

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

Comments

[nivanych]

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

[deni_ok]

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

[nivanych]

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

[deni_ok]

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

[udpn]

Где Set != Prop и Prop : Prop, например?

[nivanych]

Нет, конечно.
Можно посмотреть
http://ncatlab.org/nlab/show/fully+formal+ETCS
и пофтыкать в power object'ы.