**Steve Awodey**

**Professor**

**Departments of Philosophy and Mathematics**

**Carnegie Mellon University**

**Research Areas**

Category Theory

Logic

Philosophy of Mathematics

**Projects**

Homotopy Type Theory and Univalent Foundations. More information on this research program can be found on the site HomotopyTypeTheory.org.

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.

**Textbook**

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

·
Quillen model structures on cubical sets.

Slides from a lecture at the conference Homotopy Type Theory 2019 held at CMU, July 2019.

·
Intensionality, Invariance, and Univalence.

Slides from the 2019 Skolem Lecture held in Oslo, April 2019.

·
Impredicative Encodings in HoTT (or: Toward a Realizability ∞-Topos).

Slides from a lecture at the Isaac Newton Institute Program on Big Proof held in Cambridge, July 2017.

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

Notes from a talk at IAS, December 2010.

**Selected Preprints**

·
Sheaf Representations and Duality in Logic.

S. Awodey, June 2019.

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

S. Awodey, 2010.

·
First-order logical duality.

S. Awodey and H. Forssell, 2010.

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

·
Impredicative encodings of (higher) inductive types.

S. Awodey, J. Frey, S. Speight, *LICS*, 2018.

·
A cubical model of homotopy type theory.

S. Awodey,
*Annals of Pure and Applied Logic*, 2018.

·
Homotopy-initial algebras in type theory.

S. Awodey, N. Gambino, K. Sojakova,
*Journal of the Association for Computing Machinery*, 2017.

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

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

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

**Dissertation**

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

Ph.D.
Dissertation, The University of Chicago (1997).

[Abstract] [Summary]

**PhD Students**

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

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

· Kristina Sojakove, Higher Inductive Types as Homotopy-Initial Algebras, CMU, Computer Science, 2016.

· 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 Collected Works of Rudolf Carnap
, editor.

·
The Bernays Project
, project member.

·
The Bulletin of Symbolic Logic
, reviews managing editor (formerly).

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

**Course Materials**

**Other Links**

·
CMU Pure and Applied Logic Program

·
The HoTT Wiki

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