Steve Awodey

Professor, Philosophy and Mathematics

The Dean's Chair in Logic

Carnegie Mellon University

---

Research

• Homotopy Type Theory
• Algebraic Set Theory (Archive)

---

Books

• Homotopy Type Theory: Univalent Foundations of Mathematics. The Univalent Foundations Program, Institute for Advanced Study, 2013.

• Category Theory.
  Oxford Logic Guides 52, Oxford University Press, 2006. Second edition, 2010. Errata

---

Lectures

• Algebraic type theory Slides from a talk at the conference Category Theory 2024.

• What is HoTT? Slides from a talk for the Hausdorff Institute for Mathematics program Prospects of Formal Mathematics in May 2024. HIM video

• Cartesian cubical model categories Slides from a talk at the conference Category Theory 2023.

more...

• Homotopy type theory Slides from a talk for the CMU Philosophy Department Colloquium in September 2023.

• The isotropy group of a first-order theory Slides from a talk at the special session in memory Pieter Hofstra at the 2022 Category Theory Octoberfest.

• Kripke-Joyal forcing for Martin-Löf type theory Slides from a talk at the special session on Homotopy Type Theory at the ASL annual meeting, held at Cornell University in April 2022.

• Polynomial functors and type theory. Slides from a tutorial at the 2022 Workshop on Polynomial Functors, held online at the Topos Institute in March 2022.

• Univalence in ∞-topoi. Slides from a lecture at the conference Category Theory 2020->21, held in Genoa in August-September 2021.

• Quillen model structures on cubical sets. Slides from a lecture at the conference Homotopy Type Theory 2019, held at CMU in July 2019.

• Intensionality, Invariance, and Univalence. Slides from the 2019 Skolem Lecture, held in Oslo in April 2019.

• Impredicative Encodings in HoTT (or: Toward a Realizability ∞-Topos). Slides from a lecture at the Isaac Newton Institute Program Big Proof, held in Cambridge in July 2017.

• Recent Work in Homotopy Type Theory. Slides from a talk at an AMS meeting in January 2014.

• Homotopy Type Theory and Univalent Foundations. Slides from a talk at CMU in March 2012.

• Introduction to the Univalent Foundations of Mathematics: Constructive Type Theory and Homotopy Theory. Notes from a talk at IAS in December 2010.

---

Preprints

• The equivariant model structure on cartesian cubical sets, Steve Awodey, Evan Cavallo, Thierry Coquand, Emily Riehl, Christian Sattler, June 2024. arXiv:2406.18497

• On Hofmann-Streicher universes. S. Awodey, July 2023. arXiv:2205.10917

• Cartesian cubical model categories, May 2023. arXiv:2305.00893, preprint

more...

• Polynomial pseudomonads and dependent type theory. S. Awodey, C. Newstead, February 2018. arXiv:1802.00997

• Homotopy and type theory (Project description). October 2009. Unpublished grant proposal

• Axiom of choice and excluded middle in categorical logic. Spring 1995. Unpublished MS

---

Publications

• Kripke-Joyal forcing for type theory and uniform fibrations.
  S. Awodey, N. Gambino, S. Hazratpour, Selecta Mathematica, July 2024. arxiv2110.14576

• Sheaf representations and duality in logic. In Claudia Casadio & Philip J. Scott (eds.), Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics. Springer Verlag. pp. 39-57 (2021) arXiv:2001.09195

more...

• A proposition is the (homotopy) type of its proofs. January 2016. In: Erich H. Reck, ed. Logic, Philosophy of Mathematics, and their History: Essays in Honor of W.W. Tait. London: College Publications, 2018. arXiv:1701.02024

• Impredicative encodings of (higher) inductive types. S. Awodey, J. Frey, S. Speight, Logic in Computer Science (LICS 2018). arXiv:1802.02820

• Univalence as a principle of logic. Indagationes Mathematicae: Special Issue L.E.J. Brouwer, 50 years later, D. van Dalen, et al. (ed.s), 2018. preprint

• A cubical model of homotopy type theory. Annals of Pure and Applied Logic, 2018. arXiv:1607.06413

• Homotopy-initial algebras in type theory. S. Awodey, N. Gambino, K. Sojakova, Journal of the Association for Computing Machinery, 2017. arXiv:1504.05531

• Natural models of homotopy type theory. Mathematical Structures in Computer Science, December 2016. arXiv:1406.3219

• Topos semantics for higher-order modal logic. S. Awodey, K. Kishida, H.-C. Kotzsch, Logique & Analyse, February 2014. arXiv:1403.0020

• Univalent foundations and the large scale formalization of mathematics. S. Awodey, T. Coquand, The IAS Letter, Institute for Advanced Study, Spring 2013. pdf

• Structuralism, invariance, and univalence. Philosophia Mathematica, 2013. pdf

• Voevodsky's univalence axiom in homotopy type theory. S. Awodey, A. Pelayo, and M. Warren, Notices of the American Mathematical Sciety, 2013. pdf

• Type theory and homotopy. In Dybjer, P., Lindström, Sten, Palmgren, Erik (eds.), Epistemology versus Ontology: Essays on the Foundations of Mathematics in Honour of Per Martin-Löf. Springer, 2010. arXiv:1010.1810

• First-order logical duality. S. Awodey and H. Forssell, Annals of Pure and Applied Logic, 2013. arXiv:1008.3145

• Martin-Löf complexes. S. Awodey, P. Hofstra, M. Warren, 2009. pdf

• From sets, to types, to categories, to sets. 2009. pdf

• Algebraic models of theories of sets and classes in categories of ideals. S. Awodey, H. Forssell, M. Warren, June 2006.
  pdf

• Relating topos theory and set theory via categories of classes. S. Awodey, C. Butz, A. Simpson, T. Streicher. Bulletin of Symbolic Logic, June 2003. Research announcement

• Lawvere-Tierney sheaves in algebraic set theory. S. Awodey, N. Gambino, P. Lumsdaine, M. Warren. Journal of Symbolic Logic, 2009. pdf

• Homotopy theoretic models of identity types. S. Awodey, M. Warren. Mathematical Proceedings of the Cambridge Philosophical Society, 2009. pdf

• Relating first-order set theories, toposes and categories of classes. Steve Awodey, Carsten Butz, Alex Simpson, and Thomas Streicher. Annals of Pure and Applied Logic, 2013. pdf

• A brief introduction to algebraic set theory. The Bulletin of Symbolic Logic, 2008. pdf

• Topology and modality: The topological interpretation of first-order modal logic. S. Awodey, K. Kishida, The Review of Symbolic Logic, 2008. pdf

• Saunders Mac Lane (memorial notice). Proceedings of the American Philosophical Society, 2007. pdf

• Carnap's Dream: Gödel, Wittgenstein, and Logical Syntax. S. Awodey, A.W. Carus, Synthese, 2007. pdf

• Sheaf toposes for realizability. S. Awodey and A. Bauer, Archive for Mathemtical Logic, 2008. pdf

• Algebraic models of intuitionistic theories of sets and classes. S. Awodey and H. Forssell, Theory and Applications of Categories, 15(5), CT 2004, pp. 147--163 (2004). pdf

• Predicative algebraic set theory. S. Awodey and M. Warren, Theory and Applications of Categories, 15(1), CT 2004, pp. 1--39 (2004). pdf

• Ultrasheaves and double negation. S. Awodey and J. Eliasson, Notre Dame Journal of Formal Logic, 45(4), pp. 235--245 (2004). pdf

• Propositions as [types]. S. Awodey and A. Bauer, Journal of Logic and Computation, 14(4), pp. 447--471 (2004). pdf

• An answer to G. Hellman's question `Does category theory provide a framework for mathematical structuralism?' Philosophia Mathematica, (3), vol. 12 (2004), pp. 54--64. pdf

• Modal operators and the formal dual of Birkhoff's completeness theorem. S. Awodey and J. Hughes, Mathematical Structures in Computer Science, vol. 13 (2003), pp. 233-258.

• Categoricity and completeness: 19th century axiomatics to 21st century semantics. S. Awodey and E. Reck, History and Philosophy of Logic, 23 (2002), pp. 1-30, 77-94.

• Elementary axioms for local maps of toposes. S. Awodey and L. Birkedal, Journal of Pure and Applied Algebra, 177 (2003), pp. 215-230. pdf

• Local realizability toposes and a modal logic for computability. S. Awodey, L. Birkedal, D.S. Scott, Mathematical Structures in Computer Science, vol. 12 (2002), pp. 319-334. pdf

• Topological completeness for higher-order logic. S. Awodey and C. Butz, Journal of Symbolic Logic, 65(3), (2000) pp. 1168--82. pdf

• Topological representation of the lambda-calculus. Mathematical Structures in Computer Science, vol. 10, (2000) pp. 81--96, pdf

• Sheaf representation for topoi. Journal of Pure and Applied Algebra, 145 (2000), pp. 107--121. pdf

• Carnap, completeness, and categoricity: The Gabelbarkeitssatz of 1928. S. Awodey and A.W. Carus, Erkenntnis 54 (2001), pp. 145-172.

• Structure in mathematics and logic: a categorical perspective. Philosophia Mathematica (3), vol. 4 (1996), pp. 209--237.

• Dissertation: Logic in Topoi: Functorial Semantics for Higher-Order Logic. Ph.D. Dissertation, The University of Chicago, 1997.

---

Students

• Colin Zwanziger, The natural display topos of coalgebras, CMU, Philosophy, 2023. pdf

• Clive Newstead, Algebraic models of dependent type theory, CMU, Mathematics, 2018. pdf

• Floris van Doorn, On the formalization of higher inductive types and synthetic homotopy theory, CMU, Pure and Applied Logic, 2018. pdf

• Egbert Rijke, Classifying Types: Topics in synthetic homotopy theory, CMU, Pure and Applied Logic, 2018. pdf

• Kristina Sojakova, Higher Inductive Types as Homotopy-Initial Algebras, CMU, Computer Science, 2016. pdf

• Spencer Breiner, Scheme representation for first-logic, CMU, Pure and Applied Logic, 2014. pdf

• Peter LeFanu Lumsdaine, Higher categories from type theory, CMU, Mathematics, 2010. pdf

• Kohei Kishida, Generalized topological semantics for first-order modal logic, University of Pittsburgh, Philosophy, 2010. pdf

• Henrik Forssell, First-order logical duality, CMU, Philosophy, 2008. pdf

• Michael Warren, Homotopy-theoretic aspects of constructive type theory, CMU, Philosophy, 2008. pdf

• Matthew Jackson, A sheaf-theoretic approach to measure theory, University of Pittsburgh, Mathematics, 2006. pdf

• Jonas Eliasson, Ultrasheaves, University of Uppsala, Mathematics, 2003. pdf

• Jesse Hughes, A study of categories of algebras and coalgebras, CMU, Philosophy, 2001. pdf

---

Editorial

• Journal of Symbolic Logic
• Mathematical Logic Quarterly
• Collected Works of Rudolf Carnap
• Selected Papers of Dana Scott

---

Courses

• Category Theory
• Categorical Logic
• Topics in Logic: Type Theory
• Formal Logic
• Logic and Proof (Fischbachau Herbstschule)

---

Links

• Homotopy Type Theory 2023
• nLab
• Homotopy Type Theory
• Pure and Applied Logic
• The Carnap Blog
• Marc Awodey Memorial

---

Contact

Steve Awodey, Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA 15213 USA

Office BH 135F, Phone (412) 268-8947, Email awodey(at)cmu(dot)edu