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 higher modalities.
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, January 8, 2020, Volume 16, Issue 1 (arXiv:1706.07526, episciences:6015)
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
For an introduction from the perspective of philosophy see
David Corfield, Modal homotopy type theory, 2017 (PhilSci archive:15260)
David Corfield, Modal homotopy type theory, Oxford University Press 2020 (ISBN: 9780198853404)
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)
David Jaz Myers, Good Fibrations through the Modal Prism (arXiv:1908.08034)
Last revised on May 27, 2020 at 10:24:19. See the history of this page for a list of all contributions to it.