Math 2.0

Mathematical logic and foundations Definition

Intuitionistic type theory

Builds on Type theoryIntuitionistic logicCurry–Howard correspondence

Definition

Intuitionistic type theory, or Martin-Löf type theory, is the dependent type theory with the following parts.

  1. Four forms of judgment in a context Γ\Gamma. They say that AA is a type, or that AA and BB are equal types. They also say that aa has type AA, written a:Aa : A, or that aa and bb are equal terms of type AA.
  2. Dependent function types ∏x:AB(x)\prod_{x : A} B(x), whose terms are functions λx. b(x)\lambda x.\, b(x) with b(x):B(x)b(x) : B(x) for each x:Ax : A.
  3. Dependent pair types ∑x:AB(x)\sum_{x : A} B(x), whose terms are pairs (a,b)(a, b) with a:Aa : A and b:B(a)b : B(a).
  4. Identity types IdA(a,b)\mathrm{Id}_A(a, b) for a,b:Aa, b : A, with the reflexivity term refla:IdA(a,a)\mathrm{refl}_a : \mathrm{Id}_A(a, a) and an induction rule.
  5. Base types: the empty type 𝟎\mathbf{0}, the unit type 𝟏\mathbf{1}, the type 𝟐\mathbf{2} of booleans and the natural numbers ℕ\N. Each has introduction rules and an induction rule.
  6. Universes U0:U1:⋯U_0 : U_1 : \cdots, types whose terms are codes of types.

Each type former comes with formation, introduction, elimination and computation rules.

Remarks

Under the Curry–Howard correspondence, ∏x:AB(x)\prod_{x : A} B(x) reads as "for all xx in AA, B(x)B(x)", ∑x:AB(x)\sum_{x : A} B(x) as "there is xx in AA with B(x)B(x)", and 𝟎\mathbf{0} as falsity. Example: the term λn. (n+1,refln+1)\lambda n.\, (n + 1, \mathrm{refl}_{n+1}) has type ∏n:ℕ∑m:ℕIdℕ(m,n+1)\prod_{n : \N} \sum_{m : \N} \mathrm{Id}_{\N}(m, n + 1), so it proves that every natural number has a successor. Non-example: there is no closed term of type ∏A:U0(A+(A→𝟎))\prod_{A : U_0} (A + (A \to \mathbf{0})), so the intuitionistic logic of the theory does not include excluded middle. Martin-Löf gave several versions, with intensional or extensional identity types.

Reading path

To understand this page from the ground up, read these 33 pages in order. The foundations come first.

Show the path as a graph
Element, definition, no evidence levelElementdefinitionIntuitionistic logic, concept, no evidence levelIntuitionistic logicconceptLambda calculus, concept, no evidence levelLambda calculusconceptNatural deduction, concept, no evidence levelNatural deductionconceptProposition, concept, no evidence levelPropositionconceptSet, concept, no evidence levelSetconceptSet, definition, no evidence levelSetdefinitionConjunction, definition, no evidence levelConjunctiondefinitionDisjunction, definition, no evidence levelDisjunctiondefinitionImplication, definition, no evidence levelImplicationdefinitionNegation, definition, no evidence levelNegationdefinitionPredicate, definition, no evidence levelPredicatedefinitionOrdered pair, definition, no evidence levelOrdered pairdefinitionBiconditional, definition, no evidence levelBiconditionaldefinitionCurry–Howard correspondence, definition, no evidence levelCurry–Howard correspo…definitionTruth table, concept, no evidence levelTruth tableconceptModus ponens, concept, no evidence levelModus ponensconceptExistential quantifier, definition, no evidence levelExistential quantifierdefinitionUniversal quantifier, definition, no evidence levelUniversal quantifierdefinitionCartesian product, definition, no evidence levelCartesian productdefinitionSubset, definition, no evidence levelSubsetdefinitionPropositional logic, concept, no evidence levelPropositional logicconceptMathematical proof, concept, no evidence levelMathematical proofconceptUniqueness quantifier, definition, no evidence levelUniqueness quantifierdefinitionBinary relation, definition, no evidence levelBinary relationdefinitionTautology, definition, no evidence levelTautologydefinitionLogical equivalence, definition, no evidence levelLogical equivalencedefinitionFunction, definition, no evidence levelFunctiondefinitionDouble negation law, statement, no evidence levelDouble negation lawstatementProof by contradiction, concept, no evidence levelProof by contradictionconceptRussell's paradox, statement, no evidence levelRussell's paradoxstatementType theory, definition, no evidence levelType theorydefinitionIntuitionistic type theory, definition, no evidence levelIntuitionistic type t…definition
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Element definition
  2. Intuitionistic logic concept
  3. Lambda calculus concept
  4. Natural deduction concept
  5. Proposition concept
  6. Set concept
  7. Set definition
  8. Conjunction definition
  9. Disjunction definition
  10. Implication definition
  11. Negation definition
  12. Predicate definition
  13. Ordered pair definition
  14. Biconditional definition
  15. Curry–Howard correspondence definition
  16. Truth table concept
  17. Modus ponens concept
  18. Existential quantifier definition
  19. Universal quantifier definition
  20. Cartesian product definition
  21. Subset definition
  22. Propositional logic concept
  23. Mathematical proof concept
  24. Uniqueness quantifier definition
  25. Binary relation definition
  26. Tautology definition
  27. Logical equivalence definition
  28. Function definition
  29. Double negation law statement
  30. Proof by contradiction concept
  31. Russell's paradox statement
  32. Type theory definition
  33. Intuitionistic type theory definition

Where this leads

1 page builds on this one.

Further reading

  1. Web https://en.wikipedia.org/wiki/Intuitionistic_type_theory
About this page
TagKCV8RKBATN
URIm2://KCV8RKBATN
Kinddefinition
WritingW0 stub
MSC03B38, 03F55, 03F50
DefinesIntuitionistic type theory
UsesType theory, Intuitionistic logic, Curry–Howard correspondence
Changed2 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • an inventory row: the row of the inventory that the node accounts for (0 of 1)
  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

Used by