[Agda] Simple contradiction from type-in-type
Samuel Gélineau
gelisam at gmail.com
Thu Mar 14 01:19:19 CET 2013
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
More information about the Agda
mailing list