如何定义函子固定点？

Question

在 Haskell 中，我可以定义一个内函子固定点，因此：

data Fix f = Fix (f (Fix f))

但在 Agda 中不能：

data Fix (F : Id (Set ? Set)) : Set where
    fix : (unId F) (Fix F) ? Fix F

正如它所说的“Fix 不是严格的正数，因为它出现在 Fix 定义中构造函数 fix 类型中绑定变量的参数中。”

我尝试Coinduction.?从 stdlib 中使用，但徒劳无功：

data Fix (F : Set ? Set) : Set where
    fix : ? (F (Fix F)) ? Fix F

或者

data Fix (F : Set ? Set) : Set where
    fix : F (? (Fix F)) ? Fix F

两者都不起作用。

我发现这个文档定义了多项式函子Functor和一个有效的函数[_] : Functor ? Set ? Set：

data Functor : Set? where
    Id : Functor
    Const : Set ? Functor
    _?_ : Functor ? Functor ? Functor
    _?_ : Functor ? Functor ? Functor

[_] : Functor ? Set ? Set
[ Id ] B = B
[ Const C ] _ = C
[ F ? G ] B = [ F ] B ? [ G ] B
[ F ? G ] B = [ F ] B × [ G ] B

data Fix (F : Functor) : Set where
    fix : [ F ] (Fix F) ? Fix F

但我不确定为什么会这样，这不会，因为两者都Fix作为绑定变量的参数F。

可以在 Agda 中定义一个通用的内函子固定点吗，如果可以，如何定义？

编辑：这被标记为14699334的可能重复，但唯一的答案是链接到（？）Agda 教程，其中包括特定多项式函子类型的固定点；我想知道是否可以更一般地定义这一点。特别是，我想定义结构上可能相等但名义上不相等的类型的固定点。