**Steve Awodey**

**Professor**

**Departments of Philosophy and Mathematics**

**Carnegie Mellon University**

**Research Areas**

Category Theory, Logic, Homotopy Type Theory

**Current Projects**

Homotopy Type Theory. More information on this research program in general can be found on HomotopyTypeTheory.org.

Algebraic Set Theory. An older 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.*

**Textbook**

**
Category Theory**
, Oxford Logic Guides, Oxford University Press, 2006. Second edition, 2010.

**
**

**Slides and Resources**

Slides from a lecture at the conference International Category Theory 2020->21 held in Genoa, Italy, August-September 2021.

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

·
Kripke-Joyal forcing for type theory and uniform fibrations.

S. Awodey, N. Gambino, S. Hazratpour, October 2021.

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

·
Univalent Foundations and the Large Scale Formalization of Mathematics.

S. Awodey, T. Coquand,
*The IAS Letter*, Institute for Advanced Study, 2013.

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

·
Saunders Mac Lane (memorial notice).

S. Awodey, *Proceedings of the American Philosophical Society*, 2007.

·
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 Sojakova, 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 Journal of Symbolic Logic

·
Mathematical Logic Quarterly

·
The Collected Works of Rudolf Carnap

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