メモ

{-# OPTIONS --type-in-type #-}

module Proof where

⊥ : Set
⊥ = (A : Set) -> A

¬_ : Set -> Set
¬ A = A -> ⊥

pow : Set -> Set
pow U = U -> Set

data _==_ {A : Set} : A -> A -> Set where
  refl : (a : A) -> a == a

symm : {A : Set} -> {a b : A} -> a == b -> b == a
symm (refl x) = refl x

eq-map : {f1 f2 : Set -> Set} -> (x : Set) -> (f1 x) -> (f1 == f2) -> (f2 x)
eq-map {f1} {.f1} x f1x (refl .f1) = f1x

postulate σ : Set -> (pow Set)
postulate τ : (pow Set) -> Set
postulate ax : ∀ X -> (σ (τ X)) == X

_∈_ : Set -> Set -> Set
y ∈ x = (σ x) y

Δ : Set
Δ = τ (λ (x : Set) -> ¬ (x ∈ x))

Δ∈Δ : Set
Δ∈Δ = Δ ∈ Δ

lem1 : (x : Set) -> x ∈ Δ -> ¬ (x ∈ x)
lem1 x p = proof
  where
    p' : (λ (y : Set) -> ¬ (y ∈ y)) x
    p' = eq-map x p (ax (λ (y : Set) -> ¬ (y ∈ y)))

    proof : ¬ (x ∈ x)
    proof = p'

lem2 : Δ∈Δ -> ¬ (Δ∈Δ)
lem2 obj = lem1 Δ obj

lem3 : (x : Set) -> ¬ (x ∈ x) -> x ∈ Δ
lem3 x obj = proof
  where
    p : (σ (τ (λ (y : Set) -> ¬ (y ∈ y)))) x
    p = eq-map x obj (symm (ax (λ (y : Set) -> ¬ (y ∈ y))))

    proof' : (σ Δ) x
    proof' = p

    proof : x ∈ Δ
    proof = proof'

lem4 : ¬ (Δ∈Δ) -> Δ∈Δ
lem4 obj = lem3 Δ obj

d : ¬ (Δ∈Δ)
d = λ (y : Δ∈Δ) -> (lem2 y) y

d' : Δ∈Δ
d' = lem4 d

owata : ⊥
owata = d d'