Math 2.0

Mathematical logic and foundations Definition

Homotopy type theory

Builds on Intuitionistic type theoryIntuitionistic type theoryFunction

Definition

Start from intuitionistic type theory with intensional identity types, dependent function and pair types, and a hierarchy of universes. Homotopy type theory is this theory extended by two principles.

  1. The univalence axiom: for each universe UU and all types A,B:UA, B : U, the canonical map idtoeqv ⁣:(A=UB)→(A≃B)\mathrm{idtoeqv} \colon (A =_U B) \to (A \simeq B) is an equivalence.
  2. Higher inductive types: types given by generators for points and also for paths. An example is the circle S1S^1, generated by a point base:S1\mathrm{base} : S^1 and a path loop:base=S1base\mathrm{loop} : \mathrm{base} =_{S^1} \mathrm{base}.

Here A≃BA \simeq B is the type of equivalences, that is, of functions f ⁣:A→Bf \colon A \to B that have a two-sided inverse up to identification. The theory is read homotopically. A type is a space, a term a:Aa : A is a point, and a term p:a=Abp : a =_A b is a path from aa to bb.

Remarks

Example: in homotopy type theory one proves that the type of loops base=S1base\mathrm{base} =_{S^1} \mathrm{base} is equivalent to the integers ℤ\Z. This matches the classical fact that the fundamental group of the circle is ℤ\Z. Non-example: intuitionistic type theory with extensional identity types, where any two terms of a=Aba =_A b are equal, is not compatible with univalence. The type 𝟐\mathbf{2} of booleans has two self-equivalences, the identity and the swap. With univalence they give two paths 𝟐=𝟐\mathbf{2} = \mathbf{2}, and extensional identity types make these paths equal. Then the identity and the swap would be equal, which is false. Univalence implies function extensionality: two functions that agree at each point are equal.

Reading path

To understand this page from the ground up, read these 37 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 theorydefinitionType theory, concept, no evidence levelType theoryconceptIntuitionistic type theory, definition, no evidence levelIntuitionistic type t…definitionCurry–Howard correspondence, concept, no evidence levelCurry–Howard correspo…conceptIntuitionistic type theory, concept, no evidence levelIntuitionistic type t…conceptHomotopy type theory, definition, no evidence levelHomotopy type theorydefinition
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. Type theory concept
  34. Intuitionistic type theory definition
  35. Curry–Howard correspondence concept
  36. Intuitionistic type theory concept
  37. Homotopy type theory definition

Further reading

  1. Web https://en.wikipedia.org/wiki/Homotopy_type_theory
About this page
TagJCCTFJV9CN
URIm2://JCCTFJV9CN
Kinddefinition
WritingW0 stub
MSC03B38, 55U35, 03F55
DefinesHomotopy type theory
UsesIntuitionistic type theory, Intuitionistic type theory, Function
Changed2 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • 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

No page links to this page yet.