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, talks, and code

Higher observational type theory

• Narya: a proof assistant for higher-dimensional type theory. Code available on GitHub, and documentation on readthedocs.
• An observational proof assistant for higher-dimensional mathematics: Slides from a talk at the North American ASL Meeting in Spring 2025: [PDF].
• Higher observational type theory: Slides from a talk at Texas State University in Spring 2025: [PDF].
• Towards an implementation of Higher Observational Type Theory: slides from a talk at the Running HoTT conference in Spring 2024: [PDF]
• From HoTT to H.O.T.T.: Slides from a talk at the conference Is Philosophy Useful for Science, and/or Vice Versa? in Winter 2024 at Chapman University: [PDF].
• (with Thorsten Altenkirch, Yorgo Chamoun, and Ambrus Kaposi) Internal parametricity, without an interval. Proc. ACM Program. Lang. 8, POPL, Article 78 (January 2024): DOI and also available on the arXiv:2307.06448.
• Higher observational type theory: an autonomous foundation for univalent mathematics: Slides from a talk at Chapman University in Fall 2022: [PDF]
• Towards third-generation HoTT: Slides from talks at CMU in Spring 2022: [one], [two], [three].

Homotopy type theory

• Strange new universes: proof assistants and synthetic foundations. Bulletin of the American Mathematical Society, 2024. DOI.
• (with Astra Kolomatskaia) Displayed type theory and semi-simplicial types. Preprint available on the arXiv:2311.18781.
• (with Benedikt Ahrens, Paige Randall North, and Dimitris Tsementzis) The Univalence Principle. Book-length expansion of "A higher structure identity principle". Available on the arXiv:2102.06275.
• (with Marc Bezem, Ulrik Buchholtz, and Daniel Grayson) Construction of the Circle in UniMath. Journal of Pure and Applied Algebra 225:10, 2021. Also available on the arXiv:1910.01856.
• (with Benedikt Ahrens, Paige Randall North, and Dimitris Tsementzis) A Higher Structure Identity Principle. LICS 2020. Available on the arXiv:2004.06572. You can also see the slides from a talk I gave at Birmingham in May 2020.
• All (∞,1)-toposes have strict univalent universes. Preprint available on the arXiv:1904.07004. You can also see the slides from my talks at the 2019 Midwest HoTT seminar, the HoTT 2019 conference, the HoTTEST 2020 conference (with video), and the UCLA algebraic topology seminar .
• (with Egbert Rijke and Bas Spitters) Modalities in homotopy type theory. Logical Methods in Computer Science 16:1 (2020), available here and also on the arXiv: 1706.07526.
• (with Emily Riehl) A type theory for synthetic ∞-categories. Higher structures 1:1 (2017), available here and also on the arXiv: 1705.07442.
• (with Peter Lumsdaine) Semantics of higher inductive types. Mathematical Proceedings of the Cambridge Philosophical Society 169:1 (2020) doi and 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. In New Spaces in Mathematics: Formal and Conceptual Reflections, ed. Gabriel Catren and Mathieu Anel, Cambridge University Press, 2021; doi. Also 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 also 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 (Oxford University Press, 2018), 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, 28:6 (2018), 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. (2017), DOI. 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 (2015) p1010–1039. DOI, direct link. 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 (2015), p1203–1277, DOI, direct link. Also available on the arXiv: 1203.3253. There are also a couple of errata.

Logic and Type Theory (other than HoTT)

• Semantics of multimodal adjoint type theory. ENTICS vol. 3 (Proceedings of MFPS XXXIX). Available online at the journal which is an overlay for the arXiv:2303.02572. You can see the slides from a virtual talk I gave more or less about this at the Toposes in Mondovi conference.
• (with Daniel Gratzer and Jonathan Sterling) Strict universes for Grothendieck topoi. Available on the arXiv:2202.12012. You can see the prepared slides from the talk I gave at the Grothendieck conference at Chapman University; although I wrote on them a lot during the talk, so it may be better to watch the video.
• (with Daniel Gratzer and Jonathan Sterling) The directed plump ordering. Available on the arXiv:2202.07329.
• Large categories and quantifiers in topos theory. Revised second half of Stack semantics and the comparison of material and structural set theories, below. No preprint is available yet, but you can see the slides from a talk I gave at Cambridge University.
• A practical type theory for symmetric monoidal categories. Theory and Applications of Categories, Vol. 37, 2021, No. 25, pp 863-907. Available online at the journal web site and also on the arXiv:1911.00818.
• Comparing material and structural set theories. Annals of Pure and Applied Logic 170(4), 2019, p465–504, DOI. Also available on the arxiv:1808.05204 (note that the arXiv v3 has a less permissive license than v2, but no other changes). Revised first half of Stack semantics and the comparison of material and structural set theories, below.
• Affine logic for constructive mathematics. Bulletin of Symbolic Logic 28(3), 327-386, journal page. Also available on the arxiv:1805.07518. You can also see the slides for a talk I gave at Indiana University.
• (with Dan Licata and Mitchell Riley) A Fibrational Framework for Substructural and Modal Logics. 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 available on the arXiv: 1004.3802, and you can see the slides from two talks I gave at NovemberFest 2009 and the 2010 Annual ASL Meeting. Currently under revision and being split; the revised first half is Comparing material and structural set theories, above.

Traces and fixed point invariants

• (with Kate Ponto) The linearity of fixed point invariants. New directions in homotopy theory, Contemporary Mathematics, Vol 707 (2018). DOI, also 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 14:3 (2014), DOI and direct link, 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 8:2 (2012), pp 1–50, DOI. 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 (3), 2014, pp 248–273. DOI, arXiv: 1107.6032.

Category theory

• LNL polycategories and doctrines of linear logic. Logical Methods in Computer Science 19:2, 2023. Available here and on the arXiv.
• (with John C. Baez, Fabrizio Genovese, and Jade Master) Categories of nets. LICS 2021. Available on the arXiv:2101.04238.
• *-autonomous envelopes and 2-conservativity of duals. Presented at Linearity/TLLA 2020; paper available on the arXiv:2004.08487. You can also see the "slides" and video from an online talk I gave at ACT@UCR in April 2020, and the slides and video from a complementary online talk at the MIT Categories Seminar in May 2020.
• The 2-Chu-Dialectica construction and the polycategory of multivariable adjunctions. Theory and Applications of Categories Vol. 35, 2020, No. 4, pp 89-136. Available online at the journal web site and also on the arxiv:1806.06082.
• (with Linde Wester Hansen) Constructing symmetric monoidal bicategories functorially. Preprint available on the arXiv:1910.09240.
• 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 2012.
• 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. Mostly superseded by Constructing symmetric monoidal bicategories functorially, 1910.09240.
• 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

• The derivator of setoids. Cahiers de topologie et géométrie différentielle catégoriques, Volume LXIV, Issue 1, 29-96. Available from the journal and also at arXiv:2105.08152. There are also slides and video from a talk I gave at the Bohemian Logico-Philosophical Café.
• (with Tom Leinster) Magnitude homology of enriched categories and metric spaces. Algebraic and Geometric Topology 21, 2021. Also available at arXiv:1711.00802, and slides from a talk here.
• (with Moritz Groth) Generalized stability for abstract homotopy theories. Annals of K-Theory Vol. 6 (2021), No. 1, 1–28. Available online at the journal web site and also 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 2009; 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.
• My thesis, in 2009 under the supervision of Peter May at the University of Chicago, was entitled "Double Categories and Base Change in Homotopy Theory". It is not posted online because nearly everything in it is contained in the papers "Homotopy limits and colimits and enriched homotopy theory", "Comparing composites of left and right derived functors", and "Framed bicategories and monoidal fibrations".

Unfinished notes

• A type theory for fibred functors and polynomials, 2018. [PDF].

Expository notes and talks

• Proof assistants: Slides from a talk for students at Texas State University in Spring 2025: [PDF].
• Betti numbers via linear algebra: Notes from a guest lecture at the end of an undergraduate topology class: [PDF].
• The meaning of synthetic topology: Slides from a talk at the joint Los Angeles topology seminar at USC, 2023: [PDF]
• Complementary foundations for mathematics: when do we choose?: Slides from a talk at JMM 2022, at an AMS Special Session entitled "Competing Foundations for Mathematics: How Do We Choose?". [PDF]
• Homotopy type theory: a high-level language for invariant mathematics: Slides from a colloquium talk at Indiana University, 2019. [PDF].
• Towards elementary ∞-toposes: Slides from a talk at the Vladimir Voevodsky memorial conference, IAS, 2018. [PDF]
• 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