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, The Univalent Foundations Program, Institute for Advanced Study, 2013.
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.
A remark on Hofmann-Streicher universes. draft
Kripke-Joyal forcing for type theory and uniform fibrations.
S. Awodey, N. Gambino, S. Hazratpour, October 2021. arxiv2110.14576
Sheaf representations and duality in logic. June 2019. arXiv:2001.09195
Polynomial pseudomonads and dependent type theory. S. Awodey, C. Newstead, February 2018. arXiv:1802.00997
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 proposition is the (homotopy) type of its proofs. January 2016. arXiv:1701.02024
Homotopy and type theory (Project description). October 2009. Unpublished grant proposal
Axiom of choice and excluded middle in categorical logic. Spring 1995. Unpublished MS
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.
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
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.
Steve Awodey, Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA 15213
Office BH 135F, Phone (412) 268-8947, Fax (412) 268-1440, Email awodey(at)cmu(dot)edu