natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
A pointed type is a type equipped with a term of that type.
The categorical semantics is a pointed object.
There is a way of pointing any type $X$ by forming the sum $X+\mathbf{1}$ and taking $inr(\star_{\mathbf{1}})$ as the base point.
In the propositions as types interpretation of type theory, every pointed type represents a true proposition. Contrast this to an inhabited type, which only represents the double negation of a true proposition.
For a given type universe $\mathcal{U}$ the type of pointed types is
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Martín Escardó, Pointed types, §33.5 in: Introduction to Univalent Foundations of Mathematics with Agda [arXiv:1911.00580, webpage]
Last revised on February 4, 2023 at 11:39:18. See the history of this page for a list of all contributions to it.