The following table gives an overview over type theoretic concepts that are used in specialized type systems. The names range over terms and the names range over types. The notation (resp. ) describes the type which results from replacing all occurrences of the type variable (resp. term variable ) in by the type (resp. term ).

Type notion Notation Meaning
Product If has type , then is a pair such that has type and has type .
Sum If has type , then either is the first injection such that has type , or

is the second injection such that has type .

Function If has type and has type , then the application has type .
Intersection If has type , then has type and has type .
Union If has type , then has type or has type .
Record If has type , then has a member that has type .
Parametric If has type , then has type for any type .
Existential If has type , then has type for some type .
Dependent product If has type , then is a pair such that has type and has type .
Dependent function If has type and has type , then the application has type .
Dependent intersection[1] If has type , then has type and has type .
  1. ^ Kopylov, Alexei (2003). "Dependent intersection: A new way of defining records in type theory". 18th IEEE Symposium on Logic in Computer Science. LICS 2003. IEEE Computer Society. pp. 86–95. CiteSeerX 10.1.1.89.4223. doi:10.1109/LICS.2003.1210048.