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

[deniok]

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

{-# OPTIONS --type-in-type --without-K #-} 
module russell where

open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Empty

-- a model of set theory
data U : Set where
  set : (I : Set) → (I → U) → U

-- a set is regular if it doesn't contain itself
regular : U → Set
regular (set I f) = (i : I) → ¬ (f i ≡ set I f)

-- Russell's set: the set of all regular sets
R : U
R = set (Σ U regular) proj₁

-- R is not regular
R-nonreg : ¬ (regular R)
R-nonreg reg = reg (R , reg) refl

-- R is regular
R-reg : regular R
R-reg (x , reg) p = subst regular p reg (x , reg) p

-- contradiction
absurd : ⊥
absurd = R-nonreg R-reg

Взято отсюда:
http://www.reddit.com/r/compsci/comments/1a7g6q/a_question_on_set_classes_and_dependent_types/
http://article.gmane.org/gmane.comp.lang.agda/5002
http://hpaste.org/84029

Comments

[voidex.livejournal.com]

Ещё тут есть:

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

[deni-ok.livejournal.com]

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

[sassa-nf.livejournal.com]

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

[voidex.livejournal.com]

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

[sassa-nf.livejournal.com]

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

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

[nivanych.livejournal.com]

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

[deni-ok.livejournal.com]

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

[nivanych.livejournal.com]

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

[deni-ok.livejournal.com]

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

[udpn.livejournal.com]

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

[nivanych.livejournal.com]

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