U 的以下归纳定义被 Coq 接受，因为它可以看到 U 在 M.T U -> U 中的出现是严格正数。
Module M.
Definition T (A : Type) : Type := unit -> A.
End M.
Module N.
Inductive U : Type :=
| c : M.T U -> U.
End N.
另一方面，U 的以下归纳定义不被 Coq 接受，因为根据 M.T 的定义，它可能会出现非严格的正数。
Module Type S.
Parameter T : Type -> Type.
End S.
Module N (M : S).
Fail Inductive U : Type :=
| c : M.T U -> U.
End N.
我如何在签名S 中指定 T 的参数应该只出现严格的负数？从而防止在其定义中出现任何非严格正数的 U。
【问题讨论】：
标签： coq
这个U 类型可以看作是M.T 的最小不动点。另一种常见的编码是
Definition Mu (T : Type -> Type) := forall A, (T A -> A) -> A.
Definition U := Mu M.T.
假设T 是一个函子（严格的积极性可能意味着什么？）：
Parameter map : forall A B, (A -> B) -> T A -> T B. (* in module M *)
我们有一个构造函数和析构函数：
Definition c : M.T U -> U := fun x A f =>
f (M.map _ _ (fun y => y _ f) x).
Definition d : U -> M.T U := fun y => y _ (fun x => M.map _ _ c x).
证明它们是逆需要参数，因此没有直接的方法来证明它。如果您不想公理化它，您可以丰富T 和U 以携带参数性证据。
本质上，上述T 是函子的要求是严格肯定性条件的语义替换/近似，这是句法。
也可以使用这个新插件关闭积极性检查：
【讨论】：