Editing Type theory (section)

==== Type inhabitation ====
{{Main|Type inhabitation}}
Generally, the desired conclusion of a proof in type theory is one of [[type inhabitation]].<ref name=":1">{{cite book |author1=Henk Barendregt |url=https://books.google.com/books?id=2UVasvrhXl8C |title=Lambda Calculus with Types |author2=Wil Dekkers |author3=Richard Statman |date=20 June 2013 |publisher=Cambridge University Press |isbn=978-0-521-76614-2 |pages=1–66}}</ref> The decision problem of type inhabitation (abbreviated by <math>\exists t.\Gamma \vdash t : \tau?</math>) is: 
:Given a context <math>\Gamma</math> and a type <math>\tau</math>, decide whether there exists a term <math>t</math> that can be assigned the type <math>\tau</math> in the type environment <math>\Gamma</math>.
[[System U#Girard's paradox|Girard's paradox]] shows that type inhabitation is strongly related to the [[consistency]] of a type system with Curry–Howard correspondence. To be sound, such a system must have uninhabited types.

A type theory usually has several rules, including ones to:
* create a judgment (known as a ''context'' in this case)
* add an assumption to the context (context ''weakening'')
* [[structural rule|rearrange the assumptions]]
* use an assumption to create a variable
* define [[Reflexive relation|reflexivity]], [[Symmetric relation|symmetry]] and [[Transitive relation|transitivity]] for judgmental equality
* define substitution for application of lambda terms
* list all the interactions of equality, such as substitution
* define a hierarchy of type universes
* assert the existence of new types

Also, for each "by rule" type, there are 4 different kinds of rules

* "type formation" rules say how to create the type
* "term introduction" rules define the canonical terms and constructor functions, like "pair" and "S".
* "term elimination" rules define the other functions like "first", "second", and "R".
* "computation" rules specify how computation is performed with the type-specific functions.

For examples of rules, an interested reader may follow Appendix A.2 of the ''Homotopy Type Theory'' book,<ref name=":5" />  or read Martin-Löf's Intuitionistic Type Theory.<ref name=":3">{{Cite web|url=https://hott.github.io/HoTT-2019/images/mltt-rules.pdf|title=Rules to Martin-Löf's Intuitionistic Type Theory|access-date=2022-01-22|archive-date=2021-10-21|archive-url=https://web.archive.org/web/20211021231427/https://hott.github.io/HoTT-2019/images/mltt-rules.pdf|url-status=live}}</ref>