A type theory is a formal system in which every term has a âtypeâ, and operations in the system are restricted to acting on specific types.

A number of type theories have been used or proposed for doing homotopy type theory.

List of types in HoTT

Typically types come with four sets of inference rules. Rules allow one to conclude one set of judgements from others. A collection of judgements is typically called a context.