deniok

{-# 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

{-# IMPORT System.IO #-}

{-# IMPORT System.IO (hPutStrLn) #-}

module AbsurdTest where

data   False : Set where -- необитаемый
record True  : Set where -- синглетон

data Bool : Set where
  true  : Bool
  false : Bool

-- декодирующая функция для булева универсума
isTrue : Bool → Set
isTrue true  = True
isTrue false = False

not_ : Bool → Bool
not true  = false
not false = true

-- абсурдистская версия
lem-not²≡id₁ : (a : Bool) → isTrue (not not a) → isTrue a
lem-not²≡id₁ true p = p
lem-not²≡id₁ false ()

-- обывательская версия
lem-not²≡id₂ : (a : Bool) → isTrue (not not a) → isTrue a
lem-not²≡id₂ true  p = p
lem-not²≡id₂ false p = p

open import Data.Nat

data Fin : ℕ → Set where
  fzero : {n : ℕ} → Fin (suc n)
  fsuc  : {n : ℕ} → Fin n → Fin (suc n)

magic₁ : {A : Set} → Fin zero → A
magic₁ ()

magic₂ : {A : Set} → Fin zero → A
magic₂ n = {! !}

• Jan Malakhovski Введение в Agda.
• Evgeny Kotelnikov Зависимые типы в Haskell.
• Andrey Vlasovskikh Команда spb-archlinux на ICFP Contest 2009.