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 Auke Booij, Martín Escardó, and Peter Lumsdaine)*.**Parametricity, automorphisms of the universe, and excluded middle**. Preprint 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**. Preprint available on the arXiv: 1509.07584.*(with Dan Licata)***Adjoint logic with a 2-category of modes**. In LFCS '16. Paper available from Dan's web site here.**Univalence for inverse EI diagrams**. Preprint 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.*(with Peter Lumsdaine)***Semantics and syntax of higher inductive types**. So far, all that is available are slides from talks: at the joint meetings in 2012, the mid-atlantic topology conference in 2016, and the HoTT MURI workshop in 2016. Also relevant are the final week of the 2012 homotopy type theory seminar, the final day of the homotopy type theory minicourse, and a bunch of posts on the HoTT blog.

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

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

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

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