问题描述
我正在尝试用精益做一些类别理论。但是，我对类型理论还不是很流利，以下内容似乎并不奏效：
class pset (S: Type) :=
(point: S)
class category (?: Type) :=
(test: unit)
instance pset_category : category pset :=
{
test := ()
}
我在 category pset 处发现类型不匹配，因为 pset 的类型为 Type -> Type，而预期的类型为 Type。出了什么问题？
解决方法
我假设您希望 502 Bad Gateway 成为“pointed set”之类的东西。那么它的定义应该是
pset现在您会注意到 class pset :=
(S : Type)
(point : S)
告诉您它的类型为 #check pset。所以你仍然不能把它变成一个 Type 1，因为你只定义了“小”类别。如果您将 category 的定义中的 Type 更改为 Type*，一切都应该没问题。