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

[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

[sassa_nf]

ну....... типа да. сбило с толку, что не invert : ∀ {x X} {f : X → ⟨Set⟩} → x ∈ sets f → X. Запись-то выглядит как буд-то интересует существование зависимого типа, хотя на самом деле интересует деконструкция значения.

прикольно, да. invert - это типа axiom of choice applied.