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
quantum algorithms:
Backround
Definition
Presentation over a site
Models
In as far as a bireflective subcategory inclusion
is understood as an inclusion (via forming of zero object-bundles) of a category $\mathcal{C}$ of “classical” objects into a category $\mathcal{B}$ of bundles of infinitesimal fibers over these (as in infinitesimal cohesion), it makes sense to address the corresponding bireflecting idempotent Frobenius monad
as the modal operator which projects out the “mode of being classical”, hence the classical modality.
For example, interpreting a tangent $\infty$-topos $T \mathbf{H}$ (generally an $\infty$-topos of parameterized module spectra) as the home of a kind of higher quantum information theory (as discussed at motivic quantization and quantum circuits via dependent linear types) then its infinitesimal cohesion $\iota \,\colon\, \mathbf{H} \hookrightarrow T \mathbf{H}$ characterizes exactly the “classical objects” in the standard sense of classical vs quantum mechanics.
A modal homotopy type theoretic formulation of the classical modality $\natural \,\colon\, T \mathbf{H} \to T \mathbf{H}$ in the internal language of such tangent $\infty$-toposes is proposed in Riley, Finster & Licata (2021), its combination with a linear multiplicative conjunction $\otimes$ (and the required bunched logic) has been developed by Riley (2022) and the interpretation as a “classical modality” in the sense of classical/quantum mechanics is discussed in Myers et al. (2023).
(shape modality $\dashv$ flat modality $\dashv$ sharp modality)
$(\esh \dashv \flat \dashv \sharp )$
dR-shape modality$\dashv$ dR-flat modality
$\esh_{dR} \dashv \flat_{dR}$
(reduction modality $\dashv$ infinitesimal shape modality $\dashv$ infinitesimal flat modality)
$(\Re \dashv \Im \dashv \&)$
fermionic modality$\dashv$ bosonic modality $\dashv$ rheonomy modality
$(\rightrightarrows \dashv \rightsquigarrow \dashv Rh)$
A system of inference rules for a classical modality added to homotopy type theory has been proposed in
and combined with a linear multiplicative conjunction and the necessary bunched logic in
The role as a “classical modality” (and introducing this terminology) making the resulting linear homotopy type theory a formal quantum language is indicated in
with further exposition in:
Created on March 29, 2023 at 11:59:39. See the history of this page for a list of all contributions to it.