Steve Awodey's GitHub pages
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.
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.
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
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
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
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.
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
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