ResizingLoop.agda

{-# OPTIONS --allow-unsolved-metas #-}
open import 1Lab.Prelude hiding (_∈_; el!)

module ResizingLoop where

module _ (all-prop : ∀ {ℓ} {A : Type ℓ} → is-prop A) where

  el! : Type → Ω
  el! A = el A all-prop

  data V : Type where
    set : (A : Ω) → (∣ A ∣ → V) → V

  _∈_ : V → V → Type
  x ∈ set A f = Σ ∣ A ∣ λ i → f i ≡ x

  Ø : V
  Ø = set (el ⊥ (hlevel 1)) λ ()

  X∉Ø : {X : V} → ¬ X ∈ Ø
  X∉Ø ()

  R : V
  R = set (el! (Σ _ λ x → ¬ x ∈ x)) fst

  X∈R→X∉X : {X : V} → X ∈ R → ¬ X ∈ X
  X∈R→X∉X ((I , I∉I) , prf) elem =
    let I∈I : I ∈ I
        I∈I = subst (λ x → x ∈ x) (sym prf) elem
    in I∉I I∈I

  R∉R : ¬ R ∈ R
  R∉R R∈R = X∈R→X∉X R∈R R∈R

  X∉X→X∈R : {X : V} → ¬ X ∈ X → X ∈ R
  X∉X→X∈R X∉X = (_ , X∉X) , refl

  Russell : ⊥
  Russell = R∉R (X∉X→X∈R R∉R)

  _ = {! Russell  !}