CODEWITHSUNDEEP
type-theorylean
Tempestas Ludi
Tempestas Ludi

Reputation: 1165

Lean pass type as parameter

I am trying to do some category theory in Lean. However, I am not yet very fluent in type theory, and the following does not really seem to work:

class pset (S: Type) :=
(point: S)

class category (𝒞: Type) :=
(test: unit)

instance pset_category : category pset :=
{
  test := ()
}

I get a type mismatch at category pset, since pset has type Type -> Type, whereas it is expected to have type Type. What is going wrong?

Upvotes: 0

Views: 118

Answers (1)

jmc
jmc

Reputation: 366

I assume you want pset to be something like "pointed sets". So then its definition should be

class pset :=
(S : Type)
(point : S)

Now you will notice that #check pset tells you it has type Type 1. So you still can't make it into a category, since you only defined "small" categories. If you change Type to Type* in the definition of category, all should be good.

Upvotes: 2

Related Questions