Michael Shulman: Papers

I am interested in category theory and higher category theory and their applications to the rest of mathematics, especially homotopy theory, logic/set theory, and computer science. Here is a list of all my published papers, preprints, notes, and other stuff I've written related to math.

Blogs and wikis

• I am a co-host of The n-Category Cafe, a group blog about math, physics and philosophy, especially as they relate to higher categories. Here is a list of my blog posts.
• I am a contributor to the nLab, a research wiki for collaborative work on the same subjects, and the associated nForum.
• I also post sometimes on the Homotopy Type Theory blog (here is a list of my posts), and contribute to the associated Coq Github project.

Papers, preprints, and talks

Homotopy type theory

• (with Egbert Rijke and Bas Spitters) Modalities in homotopy type theory. Preprint available on the arXiv: 1706.07526.
• (with Emily Riehl) A type theory for synthetic ∞-categories. Preprint available on the arXiv: 1705.07442.
• (with Peter Lumsdaine) Semantics of higher inductive types. Preprint available on the arXiv: 1705.07088. You can also see the slides from my talks at the joint meetings in 2012, the mid-atlantic topology conference in 2016, and the HoTT MURI workshop in 2016.
• Homotopy type theory: the logic of space. Chapter written for the book New Spaces in Mathematics and Physics, ed. Gabriel Catren and Mathieu Anel. Available on the arXiv: 1703.03007.
• (with Auke Booij, Martín Escardó, and Peter Lumsdaine). Parametricity, automorphisms of the universe, and excluded middle. TYPES 2016; available on the arXiv: 1701.05617.
• (with Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Matthieu Sozeau, and Bas Spitters). The HoTT Library: A formalization of homotopy type theory in Coq. CPP 2017. Also available on the arXiv: 1610.04591.
• (with Kuen-Bang Hou (Favonia)) The Sefert–van Kampen Theorem in Homotopy Type Theory. CSL 2016, available here. (This is basically section 8.7 of the Homotopy Type Theory book, below.)
• Homotopy Type Theory: A synthetic approach to higher equalities. Chapter written for the book Categories for the working philosopher, edited by Elaine Landry. Available on the arXiv: 1601.05035.
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory. Mathematical Structures in Computer Science, DOI. Also available on the arXiv: 1509.07584; you can also look at the slides from my talk at CMU in March 2017.
• Univalence for inverse EI diagrams. Homology, Homotopy and Applications, 19:2 (2017), p219–249, DOI. Also available on the arXiv: 1508.02410.
• Idempotents in intensional type theory. Logical Methods in Computer Science Vol 12 No. 3. Also available on the arXiv: 1507.03634.
• The univalence axiom for elegant Reedy presheaves. Homology, Homotopy and Applications, 17:2 (2015), p81–106, DOI. Also available on the arXiv: 1307.6248.
• (as part of the Univalent Foundations Program) Homotopy Type Theory: Univalent Foundations of Mathematics. Book available here as a free PDF download, or printed and bound at cost.
• (with Benedikt Ahrens and Krzysztof Kapulkin) Univalent categories and the Rezk completion. Mathematical Structures in Computer Science, 25:05 p1010–1039. DOI. Paper and accompanying Coq code available on the arXiv: 1303.0584.
• (with Dan Licata) Calculating the fundamental group of the circle in homotopy type theory. LICS 2013. Paper and accompanying Agda code available from Dan's web site here; the paper is also on the arXiv: 1301.3443.
• (with Urs Schreiber) Quantum gauge field theory in cohesive homotopy type theory. Extended abstract, Quantum Physics and Logic 2012, arXiv: 1408.0054, also [PDF]
• Univalence for inverse diagrams and homotopy canonicity. Mathematical Structures in Computer Science, 25:05, p1203–1277, DOI. Also available on the arXiv: 1203.3253. There are also a couple of errata.

Logic and Type Theory (other than HoTT)

• Linear logic for constructive mathematics. Preprint available on the arxiv:1805.07518
• (with Dan Licata and Mitchell Riley) A Fibrational Framework for Substructural and Modal Logics. To appear in FSCD'17; available on Dan's web site here.
• (with Dan Licata) Adjoint logic with a 2-category of modes. In LFCS '16. Paper available from Dan's web site here.
• The internal logic of a 2-topos. Currently stalled and due to be re-thought from the perspective of homotopy type theory. Its status as of when I left off can be seen on my section of the nLab.
• Stack semantics and the comparison of material and structural set theories. Preprint (currently under revision) available on the arXiv: 1004.3802. Also you can see the slides from two talks I gave at NovemberFest 2009 and the 2010 Annual ASL Meeting.

Traces and fixed point invariants

• (with Kate Ponto) The linearity of fixed point invariants. Preprint available on the arXiv: 1406.7861.
• (with Kate Ponto) The linearity of traces in monoidal categories and bicategories. Theory and Applications of Categories, Vol. 31, 2016, No. 23, pp 594–689. Available at the journal web site and also at arXiv:1406.7854. You can also see the slides from my talk at PSSL93.
• (with Moritz Groth and Kate Ponto) The additivity of traces in monoidal derivators. Journal of K-Theory, available online and also on the arXiv: 1212.3277.
• (with Kate Ponto) The multiplicativity of fixed point invariants. Algebraic and Geometric Topology 14 (2014) 1275–1306; journal web site. Also available on the arXiv: 1203.0950. You can also see the slides from a talk I gave in Glasgow, Spring 2012.
• (with Kate Ponto) Duality and traces for indexed monoidal categories. Theory and Applications of Categories Vol. 26, 2012, No. 23, pp 582-659. Available from the journal web site and also here, in three formats: with color (for reading on-screen or printing in color), black and white (for printing in black and white), and compromise (can be printed b&w, but also has some color). You can also see the slides from my talk at Octoberfest 2011.
• (with Kate Ponto) Shadows and traces in bicategories. Journal of Homotopy and Related Structures 2012, pp 1-50 (sciencedirect). Also available on the arXiv: 0910.1306. You can also see the slides of a mostly expository talk I gave on this subject here.
• (with Kate Ponto) Traces in symmetric monoidal categories. A primarily expository paper, intended as background for the above papers. Expositiones Mathematicae 32 (2), 2014, pp 248–273. sciencedirect arXiv: 1107.6032.

Category theory

• Contravariance through enrichment. Theory and Applications of Categories Vol. 33, 2018, No. 5, pp 95-130. Available online at the journal web site and also on the arXiv: 1606.05058
• (with Richard Garner) Enriched categories as a free cocompletion. Advances in Mathematics 289 (2016), 1–94. Also available on the arXiv: 1301.3191, and you can look at the slides from my talk at Octoberfest '12.
• Enriched indexed categories. Theory and Applications of Categories 28 (2013), no. 21, 616–695. Available online at the journal web site and also on the arXiv: 1212.3914.
• Exact completions and small sheaves. Theory and Applications of Categories 27 (Proceedings of CT2011) (2012), no. 7, 97–173. Available online at the journal web site and also on the arXiv: 1203.4318. You can also see the slides from my talk at CT 2011.
• (with Steve Lack) Enhanced 2-categories and limits for lax morphisms. Adv. Math. 229 no. 1 (2012), 294–356 (sciencedirect); also available on the arXiv: 1104.2111.
• Not every pseudoalgebra is equivalent to a strict one. Adv. Math. 229 no. 3 (2012), 2024–2041 (sciencedirect). Also available on the arXiv: 1005.1520.
• (with Geoff Cruttwell) A unified framework for generalized multicategories. Theory and Applications of Categories 24 (2010), No. 21, 580–655. Available online at the journal web site, and also on the arXiv: 0907.2460.
• Constructing symmetric monoidal bicategories. Preprint available on the arXiv: 1004.0993.
• Extraordinary multicategories. Nothing is written yet, but here are the slides from a talk I gave at the 2010 CMS Summer Meeting. This blog post is also relevant.
• Framed bicategories and monoidal fibrations. Theory and Applications of Categories 20 (2008), no. 18, 650–738. Available online at the journal web site and also on the arXiv:0706.1286.
• (with John Baez) Lectures on n-categories and cohomology. In Towards Higher Categories, IMA Volumes in Mathematics and its Applications, Springer 2009. Based on notes I took on a series of expository talks given by John, plus an appendix. Also available on the arXiv: math.CT/0608420.

Homotopy theory

• (with Tom Leinster) Magnitude homology of enriched categories and metric spaces. Preprint available at arXiv:1711.00802, and slides from a talk here.
• (with Moritz Groth) Generalized stability for abstract homotopy theories. Preprint available on the arxiv:1704.08084.
• Reedy categories and their generalizations. Preprint available here and on the arXiv, along with accompanying Coq code (requiring only a standard Coq 8.4 install). You can also get the version without corrections of the minor errors I noticed during formalization.
• (with Moritz Groth and Kate Ponto) Mayer-Vietoris sequences in stable derivators. Homology, Homotopy and Applications 16 (1) 2014. DOI and also available on the arXiv: 1306.2072.
• Comparing composites of left and right derived functors. New York Journal of Mathematics 17 (2011), 75–125. Available online at the journal web site, and also on the arXiv: 0706.2868. I gave a talk about this at the JMM '09; you can see the slides here.
• Parametrized spaces model locally constant homotopy sheaves. Topology Appl. 155 (2008), no. 5, 412–432. Also available on the arXiv: 0706.2874.
• Homotopy limits and colimits and enriched homotopy theory. Preprint available on the arXiv: math/0610194.

Expository notes and talks

• Homotopical trinitarianism: a perspective on homotopy type theory: Slides from a talk at the Homotopy Type Theory (MRC) special session at the 2018 Joint Mathematics Meetings. [PDF]
• Down the rabbit hole: The weird and wonderful world of constructive mathematics: slides from a talk at Mathcamp 2017. [PDF]
• From the nLab to the HoTT Book: Slides from a talk at a special session at JMM 2016 "Mathematical Information in the Digital Age of Science". [PDF]
• Homotopy type theory: towards Grothendieck's dream: Slides from my talk at CT2013. [PDF].
• Internal languages for higher categories: Slides from a 15-minute talk at IAS about some of my research goals for the homotopy type theory special year. [PDF].
• The shape of infinity. Expository notes developing the Stone-Cech compactification using gauge spaces. Available on the arXiv: 1209.2735.
• Homotopy type theory minicourse: Slides from a 4-day minicourse in Swansea. [Website]
• Homotopy type theory seminar: slides from a 7-week seminar at UCSD in Winter 2012. [Website]
• Induction on Equality: slides from a talk at Mathcamp 2011. [PDF]
• Set theory for category theory. In need of revising, but still available on the arXiv: 0810.1279.
• Generators and colimit closures: notes from a talk in the category theory proseminar at Chicago. [PDF]
• Ultrafilters, Pseudotopological spaces, and Stone-Cech compactification: notes from a talk at the graduate student "pizza seminar" at Chicago on January 23, 2008. [PDF]
• Synthetic differential geometry: notes from a talk at the graduate student "pizza seminar" at Chicago on May 31, 2006. [PDF]

LaTeX Stuff

My collection of convenient basic macros that I use in writing LaTeX papers has grown so large that I maintain it in a GitHub repository. Feel free to have a look; it also contains my BibTeX database.

• basictex repository