strictly positive 是 data type 中對 constructor 的一種特殊要求形成的屬性，這是因為如果一個語言可以定義出不是 strictly positive 的 data type，就可以在 type as logic 中定義出任意邏輯，形成不一致系統。
現在我們知道為什麼我們想知道一個 data type 是不是 strictly positive 了！了解完 strictly positive 的必要性後，我們用例子來理解什麼是不一致的系統，第一個例子是 not-bad ：
Example. Not Bad [tt-0004]
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 (
) 本來應該是不可能有任何元素的，即不存在 x 滿足 x : Bottom 這個 judgement，但我們卻成功的建構出 notBad isBad : Bottom。如此一來我們的型別對應到的邏輯系統就有了缺陷。
Example. Loop [tt-0005]
Example. Loop [tt-0005]
現在我們關心一下第二個例子 loop（修改自 Certified Programming with Dependent Types）：
data Term
abs : (Term → Term) → Term
app : Term → Term → Term
app (abs f) t = f t
w : Term
w = abs (λ x → app x x)
loop : Term
loop = app w w
loop 的計算永遠都不會結束，然而證明器用到的 dependent type theory 卻允許型別依賴 loop 這樣的值，因此就能寫出讓 type checker 無法停止的程式。換句話說，證明器仰賴的性質缺失。事實上 Term 跟 Bad 的問題就是違反了 strictly positive 的性質，或許也有人已經發現了兩者 constructor 型別的相似之處。接下來我們來看為什麼這樣的定義會製造出不一致邏輯。