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.

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

*(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.

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

*(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.

**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**. In*n*-categories and cohomology*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.

*(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.

**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]

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.