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
The smash product type is an axiomatization of the smash product in the context of homotopy type theory.
The smash product type of two pointed types $A,B$ can be defined as the pushout type of the span
where $A \vee B \rightarrow A \times B$ is the inclusion of the wedge sum type in the product type both of which are pointed. The resulting pushout is denoted the smash product $A \wedge B$ and is pointed by $\star_{A \wedge B}\equiv\mathrm{inl}(\star_{\mathbf 1})$
It can also be defined as the pushout type of the span
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Floris van Doorn (2018), On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory, (arXiv:1808.10690, web)
Kuen-Bang Hou, Higher-Dimensional Types in the Mechanization of Homotopy Theory, Ph. D. Thesis 2017 (web)
Last revised on March 6, 2023 at 20:40:50. See the history of this page for a list of all contributions to it.