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
homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
The refinement of modal type theory to homotopy type theory: hence homotopy type theory equipped with modalities as in modal logic (and in modal type theory).
There are a number of different but equivalent ways to define a modality in homotopy type theory. From Rijke, Shulman, Spitters 17:
an induction principle of type
for any type $A$ and type $B$ depending on $LA$
a computation rule
a witness that for any $x, y : LA$, the modal unit $(-)^L : (x = y) \to L(x = y)$ is an equivalence.
Uniquely eliminating modality: A modality consists of a modal operator and modal unit such that operation
is an equivalence for all types $A$ and types $B$ depending on $LA$.
$\Sigma$-closed reflective subuniverse (aka localization): A reflective subuniverse (a.k.a. localization) consists of a proposition $isLocal : {Type} \to {Prop}$ together with an operator $L : {Type} \to {Type}$ and a unit $(-)^L : X \to LX$ such that $LX$ is local for any type $X$ and for any local type $Z$, then function
is an equivalence. A localization is $\Sigma$-closed if whenever $A$ is local and for all $a : A$, $B(a)$ is local, then the dependent sum $\Sigma_{a : A} B(a)$ is local.
Stable factorization systems: A modality consists of an orthogonal factorization system $(\mathcal{L}, \mathcal{R})$ in which the left class is stable under pullback.
A localization (reflective subuniverse) whose units $(-)^L : X \to LX$ are $L$-connected.
We say that a type $X$ is $L$-modal if the unit $(-)^L : X \to LX$ is an equivalence. We say a type $X$ $L$-connected if $LX$ is contractible.
In terms of the other structure, the stable factorization system associated to a modality $L$ has
left class the $L$-connected maps, whose fibers are $L$-connected.
right class the $L$-modal maps, whose fibers are $L$-modal.
Conversely, given a stable factorization system, the modal operator and unit are given by factorizing the terminal map.
See also the references at modal type theory.
Dan Licata, Felix Wellen, Synthetic Mathematics in Modal Dependent Type Theories, tutorial at Types, Homotopy Theory and Verification (2018)
Tutorial 1, Dan Licata: A Fibrational Framework for Modal Simple Type Theories (recording)
Tutorial 2, Felix Wellen: The Shape Modality in Real cohesive HoTT and Covering Spaces (recording)
Tutorial 3, Dan Licata: Discrete and Codiscrete Modalities in Cohesive HoTT (recording)
Tutorial 4, Felix Wellen, Discrete and Codiscrete Modalities in Cohesive HoTT, II (recording)
Tutorial 5, Dan Licata: A Fibrational Framework for Modal Dependent Type Theories (recording)
Tutorial 6, Felix Wellen: Differential Cohesive HoTT, (recording)
Dan Licata, Synthetic Mathematics in Modal Dependent Type Theories, notes for tutorial at Types, Homotopy Theory and Verification, 2018 (pdf)
Univalent Foundations Project, section 7.7 of Homotopy Type Theory – Univalent Foundations of Mathematics
Mike Shulman, Higher modalities, talk at UF-IAS-2012, October 2012 (pdf)
Egbert Rijke, Mike Shulman, Bas Spitters, Modalities in homotopy type theory, Logical Methods in Computer Science, 16 1 (2020) [arXiv:1706.07526, doi:10.23638/LMCS-16(1:2)2020]
Mike Shulman, http://homotopytypetheory.org/2015/07/05/modules-for-modalities/ (2015)
Egbert Rijke, Bas Spitters, around def. 1.11 of Sets in homotopy type theory (arXiv:1305.3835)
Kevin Quirin and Nicolas Tabareau, Lawvere-Tierney Sheafification in Homotopy Type Theory, Workshop talk 2015 (pdf), Kevin Quirin thesis
For a discussion of the reflective factorization system generated by a modality, see
See also
Outlook in view of cohesive homotopy type theory:
Introduction from the perspective of philosophy:
David Corfield, Modal homotopy type theory, 2017 (PhilSci archive:15260)
David Corfield, Modal homotopy type theory, Oxford University Press 2020 (ISBN: 9780198853404)
Specifically for localization in the classical sense of algebraic topology:
Specifically for cohesive homotopy type theory see:
Urs Schreiber, Michael Shulman, Quantum gauge field theory in Cohesive homotopy type theory, in Ross Duncan, Prakash Panangaden (eds.) Proceedings 9th Workshop on Quantum Physics and Logic, Brussels, Belgium, 10-12 October 2012 (arXiv:1408.0054)
Mike Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)
Felix Wellen, Cartan Geometry in Modal Homotopy Type Theory (arXiv:1806.05966, thesis pdf following Schreiber 15)
David Jaz Myers, Good Fibrations through the Modal Prism (arXiv:1908.08034)
Formalization of the shape/flat-fracture square (differential cohomology hexagon) in cohesive homotopy type theory:
David Jaz Myers, Modal Fracture of Higher Groups, talk at CMU-HoTT Seminar, 2021 (pdf, pdf)
David Jaz Myers, Modal Fracture of Higher Groups (arXiv:2106.15390)
See also the proof of the Blakers-Massey theorem for modalities in this generality:
Last revised on July 29, 2023 at 16:03:16. See the history of this page for a list of all contributions to it.