不，在這種情況下，困境和單調性並不密切相關。

Coq/Adga中的積極性檢查可以確保您大致采用單調內容的最小固定點。

以下是如何根據格子和單調算子來考慮歸納類型。回想一下Knaster-Tarski定理說在一個完整的格子$ L $上，每個單調運算符$ f：L \到L $的固定點最小$ \ mu（f）$。接下來，我們可以將類型理論中的類型視為在可證明性下形成晶格。也就是說，如果$ S $的真值需要$ T $，則$ S $類型低於$ T $。現在，我們想要做的是在類型上采用單調運算符$ F $，並使用Knaster-Tarski來解釋此運算符$ \ mu（F）$的最小固定點。

然而，類型理論中的類型不僅僅是一個格子：它們形成一個類別。也就是說，給定兩種類型$ S $和$ T $，$ S $可能多種方式低於$ T $，每種證據都有一種方式$ e：S \ to T $。因此，類型運算符$ F $也必須對這些證明做一些明智的事情。單調性的適當推廣是 functoriality 。也就是說，我們希望$ F $在類型上有一個操作符，並且還要對證據進行操作，這樣如果$ e：S \到T $，那麽$ F（e）：F（S）\到F （T）$。

現在，functoriality由sums和產品保留（即，如果$ F $和$ G $是類型的endofunctors，那麽$ F + G $和$ F \ times G $（代表逐點）也是類型的仿函數（假設我們在代數類型中有總和和乘積。但是，它沒有被函數空間保留，因為指數分數$ F \到G $在左邊的參數中是逆變的。所以當你寫一個歸納類型定義時，你為了確保它確實是一個仿函數，你需要排除函數空間左側的遞歸參數的出現 - 從而進行積極性檢查。

通常避免不可信度（在系統F的意義上），因為它是一個迫使您在經典邏輯和集合理論模型之間進行選擇的原則。如果你有F風格的索引，你不能將類型解釋為經典集合論中的集合。 （參見雷諾茲著名的“多態性不是理論上的”。）

分類上，F風格的不可信度表示類型和術語的類別形成一個小的完整類別（即，homs和對象都是集合，並且存在所有小圖的限制）。經典地，這迫使一個類別成為一個集合。許多建構主義者都是建設性的，因為他們希望他們的定理能夠包含在更多系統而不僅僅是經典邏輯中，因此他們不想證明任何經典錯誤的東西。因此，他們對不可預測的多態性持懷疑態度。

但是，多態性允許你在類型理論的內部說出經典“大”的許多條件 - 積極性就是其中之一！類型運算符$ F $是functorial，如果你可以產生一個多態的術語：

$$ \ mathsf {Fmap}：\ forall \ alpha，\ beta。\; （\ alpha \ to \ beta）\ to（F（\ alpha）\ to F（\ beta）） $$

看看它如何與functoriality相對應？ IMO，這對於Coq來說是一個非常好的選擇，因為它可以讓你更容易地進行通用編程。積極性檢查的句法性質是泛型編程的一大障礙，我很樂意將經典公理的可能性換成更靈活的函數式程序。

編輯：你問的關於Prop和Set之間區別的問題源於Coq開發人員希望允許你想要在幼稚的集理論術語中考慮Coq定理的事實，如果你願意的話，沒有強制你這樣做。從技術上講，他們拆分Prop和Set，然後根據Prop的計算內容禁止集合。

因此，您可以將Prop解釋為ZFC中的真值，這是布爾值的真假。在這個世界上，命題的所有證明都是平等的，顯然你不應該在命題的證明上分支。因此，根據Prop的證明的計算內容禁止集合是完全合理的。此外，2元素布爾晶格顯然是一個完整的晶格，因此它應該支持impredicative索引，因為存在任意的集值。集合的困境限制源於上述事實（如上所​​述）F樣式索引在經典集合理論模型中是簡並的。

Coq有其他模型（它是建設性的邏輯！）但重點是，現成的它永遠不會證明古典數學家會被困惑的東西。