(in category theory/type theory/computer science)
of all homotopy types
of (-1)-truncated types/h-propositions
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
In homotopy type theory, the axiom of replacement states that given a type universe , for every essentially -small type , every locally -small type , and every function , the image is essentially -small.
Equivalently, given types and and Tarski universe , there is a function
Egbert Rijke, The join construction, 26 Jan 2017, (arXiv:1701.07538)
Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, Daniel R. Grayson, Section 2.19 in: Symmetry (2021) pdf
Last revised on July 18, 2023 at 20:00:39. See the history of this page for a list of all contributions to it.