[Agda] Simple contradiction from type-in-type

[Samuel Gélineau]

There was a thread [1] on Reddit/compsci today about Agda's Set hierarchy
and the paradoxes type-in-type entails. I found a simple one based on
Curry's paradox, and I am being told that such short examples are unusual
enough that I should post it here. So, here goes!

    open import Data.Empty
    open import Relation.Binary.PropositionalEquality hiding (subst)

    subst : (P : Set → Set) → {x y : Set} → x ≡ y → P y → P x
    subst P refl p = p


    data Con : Set where
      -- curry's paradox would use this.
      --   mkCon : (Con → ⊥) → Con
      -- since we have type-in-type but not negative occurrences,
      -- fake it using propositional equality.
      con : (A : Set) → Con ≡ A → (A → ⊥) → Con

    mkCon : (Con → ⊥) → Con
    mkCon f = con Con refl f

    unCon : Con → (Con → ⊥)
    unCon (con A eq f) = subst (λ x → x → ⊥) eq f

    δ : Con → ⊥
    δ c = unCon c c

    ω : ⊥
    ω = δ (mkCon δ)


[1]
http://www.reddit.com/r/compsci/comments/1a7g6q/a_question_on_set_classes_and_dependent_types/

– Samuel Gélineau
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130313/d4b022de/attachment.html