term of a type cannot be a type?

Stream: new members

[Shanghe Chen]

Hi! I am a layman in type theory, got some naive impresion that "every type is a term but some term is a type", while in the following code we cannot treat β as a type?:

universe u
variable (α : Type u)
variable (β : α)
variable (γ : β)
-- type expected, got
--   (β : α)

[Shanghe Chen]

But this work with some inductive family:

universe v
inductive TermAsType {α : Type u} : α -> Type v where
| term : (a : α) -> TermAsType a

variable (γ : TermAsType β)

[Shanghe Chen]

Any reason for this? why do we need some explicit inductive for treating terms of α as a type?

[Kevin Buzzard]

β might not be a type (eg if α is Nat and β is 37). But TermAsType β is a type because TermAsType eats a term and returns a type.

[Shanghe Chen]

Yeah intuitively it seems working in this way. I get it that a term is a type only if it’s a term of some type u. Btw I quoted “everything is a term. But some terms are types” from https://xenaproject.wordpress.com/2020/06/20/mathematics-in-type-theory/ . Thank you very much Kevin:tada: