nLab modal homotopy type theory

Idea

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).

Definitions

There are a number of different but equivalent ways to define a modality in homotopy type theory. From Rijke, Shulman, Spitters 17:

• Higher modality: A modality consists of a modal operator $L : {Type} \to {Type}$ and for every type $X$ a modal unit $(-)^L : X \to LX$ together with

1. an induction principle of type

   $$\text{ind} : ((a : A) \to LB(a^L)) \to ((u : LA) \to LB(u))$$

   for any type $A$ and type $B$ depending on $LA$

2. a computation rule

   $$\text{com} : \text{ind}(f)(a^L) = f(a).$$

3. 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

  $$f \mapsto f \circ (-)^L : ((u : LA) \to LB(u)) \to ((a : A) \to LB(a^L))$$

  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

  $$f \mapsto f \circ (-)^L : (LA \to Z) \to (A \to Z)$$

  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.

Related concepts

• reflective subuniverse

• stable homotopy type

• equivariant homotopy type

• geometric homotopy type theory

• cohesive homotopy type theory

• directed homotopy type theory

References

See also the references at modal type theory.

Review

• 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)

General

• UF-IAS-2012, Modal type theory

• 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

• Felix Cherubini, Egbert Rijke, Modal Descent, Mathematical Structures in Computer Science 31 4 (2021) 363-391 [arXiv:2003.09713, doi:10.1017/S0960129520000201]

See also

• J. Daniel Christensen, Egbert Rijke, Characterizations of modalities and lex modalities (arXiv:2008.03538)

Outlook in view of cohesive homotopy type theory:

• Urs Schreiber, Some thoughts on the future of modal homotopy type theory , talk at: Homotopy Type Theory and Univalent Foundations - Mini-Symposium, within the German Mathematical Society meeting 2015 21st - 25th Sept 2015, Hamburg (pdf notes)

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:

• J. Daniel Christensen, Morgan Opie, Egbert Rijke, Luis Scoccola, Localization in Homotopy Type Theory, Higher Structures, 4(1) (2020), 1-32 (arXiv:1807.04155)

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:

• Mathieu Anel, Georg Biedermann, Eric Finster, André Joyal, A Generalized Blakers-Massey Theorem, Journal of Topology 13 4 (2020) 1521-1553 $[$arXiv:1703.09050, doi:10.1112/topo.12163$]$