Steve Awodey
Department of Philosophy
Carnegie Mellon University

Research Areas

    Category Theory
    Philosophy of Mathematics
    Early Analytic Philosophy

Current Projects

Homotopy Type Theory and Univalent Foundations. More information on this research program can be found on the site Information on the special year 2012-13 on Univalent Foundations at the Institute for Advanced Study can be found on the UF-wiki.

Algebraic Set Theory. A website containing some information about AST and links to some papers.

The HoTT Book

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

Click here for more information.


    Category Theory, Oxford Logic Guides, Oxford University Press, 2006.
      Second edition 2010, now in paperback!

Click here for more information.

Click here for a list of errata.

Slides and Resources

·  A Cubical Model of Homotopy Type Theory. 

Notes from a series of lectures to the Stockholm Logic Group, June 2016.

·  Recent Work in Homotopy Type Theory. 

Slides from a talk at an AMS meeting, January 2014.

·  Homotopy Type Theory and Univalent Foundations.

Slides from a talk at CMU, March 2012.

·  Introduction to the Univalent Foundations of Mathematics: Constructive Type Theory and Homotopy Theory.

Notes from a talk at IAS, December 2010.

Selected Current Preprints

·  A proposition is the (homotopy) type of its proofs.    

S. Awodey, January 2016.

·  Univalence as a principle of logic.    

S. Awodey, October 2016.

·  Natural models of homotopy type theory.    

S. Awodey, December 2016.

·  Topos semantics for higher-order modal logic.    

S. Awodey, K. Kishida, H.-C. Kotzsch, 2014.

·  Structuralism, invariance, and univalence.    

S. Awodey, 2013.

·  Voevodsky's univalence axiom in homotopy type theory.    

S. Awodey, A. Pelayo, and M. Warren, 2013.

·  Type theory and homotopy.    

S. Awodey, 2010.

·  First-order logical duality.    

S. Awodey and H. Forssell, 2010.

·  Martin-Löf complexes.    

S. Awodey, P. Hofstra, M. Warren, 2009.

·  From sets, to types, to categories, to sets.    

S. Awodey, 2009.

·  Algebraic models of theories of sets and classes.    

S. Awodey, H. Forssell, M. Warren, June 2006.

·  Relating topos theory and set theory via categories of classes.    

S. Awodey, C. Butz, A. Simpson, T. Streicher, June 2003.

Research announcement. Bulletin of Symbolic Logic.


Selected Publications

·  Lawvere-Tierney sheaves in algebraic set theory.    

S. Awodey, N. Gambino, P. Lumsdaine, M. Warren, Journal of Symbolic Logic, 2009.

·  Homotopy theoretic models of identity types.    

S. Awodey, M. Warren, Mathematical Proceedings of the Cambridge Philosophical Society, 2009.

·  A brief introduction to algebraic set theory.    

S. Awodey, The Bulletin of Symbolic Logic, 2008.

·  Topology and modality: The topological interpretation of first-order modal logic.    

S. Awodey, K. Kishida, The Review of Symbolic Logic, 2008.

·  Carnap's Dream: Gödel, Wittgenstein, and Logical Syntax.    

S. Awodey, A.W. Carus, Synthese, 2007.

·  Sheaf toposes for realizability (2004).    

S. Awodey and A. Bauer, Archive for Mathemtical Logic, 2008.

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

·  Predicative algebraic set theory.    

S. Awodey and M. Warren, Theory and Applications of Categories 15(1), CT 2004, pp. 1--39 (2004).

·  Ultrasheaves and double negation.    

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

·  Propositions as [types].    

S. Awodey and A. Bauer, Journal of Logic and Computation 14(4), pp. 447--471 (2004).

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

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

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

·  Topological completeness for higher-order logic.    

S. Awodey and C. Butz, Journal of Symbolic Logic 65(3), (2000) pp. 1168--82.

·  Topological representation of the lambda-calculus.    

Mathematical Structures in Computer Science (2000), vol. 10, pp. 81--96.

·  Sheaf representation for topoi.    

Journal of Pure and Applied Algebra 145 (2000), pp. 107--121.

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

·  Axiom of choice and excluded middle in categorical logic.   

Unpublished MS (1995).


·  Logic in Topoi: Functorial Semantics for Higher-Order Logic    

Ph.D. Dissertation, The University of Chicago (1997).
              [Abstract] [Summary]

PhD Students

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

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

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

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

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

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

·  Jonas Eliasson, Ultrasheaves, University of Uppsala, Mathematics, 2003.

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

Editorial Activities

·  The Bulletin of Symbolic Logic , reviews managing editor.

·  The Collected Works of Rudolf Carnap, editor.  

·  Full Circle: Publications of the Archives of Scientific Philosophy, managing editor.  

·  The Bernays Project, project member.

Course Materials

·  Category Theory  

·  Categorical Logic  

·  Logic and Computation

Other Links

·  Pure and Applied Logic Program
·  Philosophy Department
·  The Carnap Blog
·  Marc Awodey Memorial

Contact Information

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

Office: BH 135F
Phone: (412) 268-8947
Fax: (412) 268-1440
E-Mail: awodey(at)