<div dir="ltr"><div style>There was a thread [1] on Reddit/compsci today about Agda&#39;s Set hierarchy and the paradoxes type-in-type entails. I found a simple one based on Curry&#39;s paradox, and I am being told that such short examples are unusual enough that I should post it here. So, here goes!</div>

<div style><br></div><div style><div>    open import Data.Empty</div><div>    open import Relation.Binary.PropositionalEquality hiding (subst)</div><div>    </div><div>    subst : (P : Set → Set) → {x y : Set} → x ≡ y → P y → P x</div>

<div>    subst P refl p = p</div><div><div>    </div></div><div>    </div><div>    data Con : Set where<br></div><div>      -- curry&#39;s paradox would use this.</div><div>      --   mkCon : (Con → ⊥) → Con</div><div>      -- since we have type-in-type but not negative occurrences,</div>

<div>      -- fake it using propositional equality.</div><div>      con : (A : Set) → Con ≡ A → (A → ⊥) → Con</div><div>    </div><div>    mkCon : (Con → ⊥) → Con<br></div><div>    mkCon f = con Con refl f</div><div>    </div>

<div>    unCon : Con → (Con → ⊥)<br></div><div>    unCon (con A eq f) = subst (λ x → x → ⊥) eq f</div><div>    </div><div>    δ : Con → ⊥<br></div><div>    δ c = unCon c c</div><div>    </div><div>    ω : ⊥<br></div><div>

    ω = δ (mkCon δ)</div></div><div style><br></div><div style><br></div><div style>[1] <a href="http://www.reddit.com/r/compsci/comments/1a7g6q/a_question_on_set_classes_and_dependent_types/">http://www.reddit.com/r/compsci/comments/1a7g6q/a_question_on_set_classes_and_dependent_types/</a><br>

</div><br clear="all"><div>– Samuel Gélineau<div><br></div>
</div>
</div>