The name of a type - why?

Question

Can anyone explain me this:

singleton : (t : Type) -> t -> HList [t]

Why do is "t" used here? Does t refer to an instance of the type Type?

But why not merely do this:

singleton : Type -> Type -> HList [Type]

Answer 1

singleton : (t : Type) -> t -> HList [t]

takes two parameters - a type and a value of that type e.g.

singleton Int 3 : HList [Int]
singleton String "string" : HList [String]

In contrast

singleton : Type -> Type -> HList [Type]

would take two Type parameters e.g.

singleton Int String

However assuming you're defining a HList it is probably defined as:

data HList : List Type -> Type where
  Nil : HList []
  singleton : (t : Type) -> t -> HList [t]
  ...

so it needs to be parameterised by a list of types indexing the values. Your singleton constructor would not be valid since Type is not a value of the Type type.