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
An implicative tripos is a tripos built out from an implicative algebra. It thus captures the particular logic encoded within such a structure.
Implicative triposes are triposes of $H$-valued sets for the Heyting algebra $H$ induced by the implicative algebra one started with (see implicative algebra).
In (Miquel’20b), it is proven all triposes on $\mathbf{Set}$ arise in this way, which means implicative algebras play, for ($\mathbf{Set}$-)triposes, the same role complete Heyting algebras (thus locales) play for Grothendieck toposes.
(…)
Alexandre Miquel, Implicative algebras: a new foundation for realizability and forcing, Mathematical Structures in Computer Science 30 (5): 458–510. (doi).
Alexandre Miquel. 2020. Implicative Algebras II: Completeness w.r.t. Set-Based Triposes. arXiv. https://doi.org/10.48550/arXiv.2011.09085. (arxiv)
Last revised on April 30, 2023 at 04:26:53. See the history of this page for a list of all contributions to it.