(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.
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 June 16, 2022 at 09:51:47. See the history of this page for a list of all contributions to it.