Example. Not Bad [tt-0004]

data Bad
  bad : (Bad → Bottom) → Bad

notBad : Bad → Bottom
notBad (bad f) = f (bad f)

isBad : Bad
isBad = bad notBad

absurd : Bottom
absurd = notBad isBad

Bottom ($\bot$ ) 本來應該是不可能有任何元素的，即不存在 x 滿足 x : Bottom 這個 judgement，但我們卻成功的建構出 notBad isBad : Bottom。如此一來我們的型別對應到的邏輯系統就有了缺陷。