We describe the use of Narrowing in the Omega type system. Omega is a language with an infinite hierarchy of computational levels: value, type, kind, sort, etc. Computation at the value level is performed by reduction, and computation at all higher levels is performed by narrowing.

Terms at each level are classified by terms at the next level. Thus values are classified by types, types are classified by kinds, kinds are classified by sorts, etc. Programmers are allowed to introduce new terms at every level, but any particular program will have terms at only a finite number of levels.

We formalize properties of programs by exploiting the Curry-Howard isomorphism. Terms at computational level n, are used as proofs about terms at level (n+1). We use indexed types to maintain a strict and formal connection between the two levels.