- Homotopy Type Theory
- Algebraic Set Theory (Archive)
- Homotopy Type Theory: Univalent Foundations of Mathematics. The Univalent Foundations Program, Institute for Advanced Study, 2013.
- Category Theory.
Oxford Logic Guides 52, Oxford University Press, 2006. Second edition, 2010. Errata
-
Toward the Effective 2-Topos Slides from a talk at the conference Categorical Logic and Higher Categories held in Manchester in December 2024.
-
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
more...
-
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
more...
-
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
more...
-
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.
- Dissertation: Logic in Topoi: Functorial Semantics for Higher-Order Logic. Ph.D. Dissertation, The University of Chicago, 1997.
-
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
- Journal of Symbolic Logic
- Mathematical Logic Quarterly
- Collected Works of Rudolf Carnap
- Selected Papers of Dana Scott
- Category Theory
- Categorical Logic
- Topics in Logic: Type Theory
- Formal Logic
- Logic and Proof (Fischbachau Herbstschule)
- Homotopy Type Theory 2023
- nLab
- Homotopy Type Theory
- Pure and Applied Logic
- The Carnap Blog
- Marc Awodey Memorial
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