Editing Type theory (section)

===Judgments===
Most type theories have 4 judgments:

* "<math>T</math> [[#Gamma,IsaType|is a type]]"
* "<math>t</math> [[#Gamma,IsaTerm|is a term]] of type <math>T</math>"
* "Type <math>T_1</math> [[#Gamma,IsEq|is equal to]] type <math>T_2</math>"
* "Terms <math>t_1</math> and <math>t_2</math> both of type <math>T</math> [[#Gamma,BothTsAreEq|are equal]]"

Judgments may follow from assumptions. For example, one might say "assuming <math>x</math> is a term of type <math>\mathsf{bool}</math> and <math>y</math> is a term of type <math>\mathsf{nat}</math>, it follows that <math>(\mathrm{if}\,x\,y\,y)</math> is a term of type <math>\mathsf{nat}</math>". Such judgments are formally written with the [[Turnstile (symbol)|turnstile symbol]] <math>\vdash</math>.

<math>x:\mathsf{bool},y:\mathsf{nat}\vdash(\textrm{if}\,x\,y\,y): \mathsf{nat}</math>

If there are no assumptions, there will be nothing to the left of the turnstile.

<math>\vdash \mathrm{S}:\mathsf{nat}\to\mathsf{nat}</math>

The list of assumptions on the left is the ''context'' of the judgment. Capital greek letters, such as [[Gamma|<math>\Gamma</math>]] and <math>\Delta</math>, are common choices to represent some or all of the assumptions. The 4 different judgments are thus usually written as follows.

{| class="wikitable"
! Formal notation for judgments !! Description
|- {{anchor|Gamma,IsaType}}
|<math>\Gamma \vdash T</math> Type||<math>T</math> is a type (under assumptions <math>\Gamma</math>).
|- {{anchor|Gamma,IsaTerm}}
|<math>\Gamma \vdash t : T</math>||<math>t</math> is a term of type <math>T</math> (under assumptions <math>\Gamma</math>).
|- {{anchor|Gamma,IsEq}}
|<math>\Gamma \vdash T_1 = T_2 </math>||Type <math>T_1</math> is equal to type <math>T_2</math> (under assumptions <math>\Gamma</math>).
|- {{anchor|Gamma,BothTsAreEq}}
|<math>\Gamma \vdash t_1 = t_2 : T </math>||Terms <math>t_1</math> and <math>t_2</math> are both of type <math>T</math> and are equal (under assumptions <math>\Gamma</math>).
|}

Some textbooks use a triple equal sign <math>\equiv</math> to stress that this is [[Judgment (mathematical logic)|judgmental equality]] and thus an [[Intrinsic and extrinsic properties|extrinsic]] notion of equality.<ref name=":5">{{Cite book |last=The Univalent Foundations Program |url=https://homotopytypetheory.org/book/ |title=Homotopy Type Theory: Univalent Foundations of Mathematics |publisher=Homotopy Type Theory |year=2013}}</ref> The judgments enforce that every term has a type. The type will restrict which rules can be applied to a term.