Glossary¶
- type
- object
- space
- object
Type and space are synonyms. Object may be used as another synonym, but it may also refer to the interpretation of contexts in the chosen Categorical semantics.
See also Types as spaces.
- constructor
- element
- point
- term
- proof
- element
- See Constructors vs elements vs points vs terms vs proofs.
- proposition
- hproposition
- A type with the property that all its elements are equal.
- pointed type
- A pointed type is a type \(X\) together with a point of \(X\). In other words, a pointed type is an element of \(\sum_{X:\mathcal{U}}X\).
- principle of excluded middle
- weak excluded middle
- These two axioms decide the truth of any proposition \(P\) to various degrees. Whereas the principle of excluded middle says that, given a proposition \(P\), we can decide the truth of \(P\), that is, we get \(P+\neg P\), weak excluded middle only says we can decide the truth of \(\neg P\), that is, it tells us \(\neg P + \neg \neg P\).
- context
- All mathematical claims are made in a certain context. For example, “\(\phi\) is an isomorphism that sends \(g\) to \(h(x)+3\)” only makes sense if we know that \(\phi\), \(g\) and \(h\) are variables of a certain type. In the logic of type theory, the concept of contexts plays an extremely central role, and the truth and interpretation of every type and term depends on the context we’re in. So a context is just a list of fresh variables with type declarations. For more information, see e.g. Appendix A.2 of the HoTT book, or a source on semantics of type theory such as [Hof97].
- HIT
- higher-inductive type
- See chapter 6 of the HoTT book.
- n-type
- truncated type
- See chapters 3 and 7 of the HoTT book.
- axiom
- An axiom is added to a type theory by adding a new symbol to the language without any computation rules. Function extensionality and univalence are added as axioms in section A.3.1 of the HoTT book.
- extensionality
- The idea that if two objects behave equally, then they are equal as objects. Function extensionality specifies that functions are equal if they have the same input-output behavior.