nLab Steve Awodey

Steve Awodey is a professor at Carnegie Mellon University interested in category theory, logic, philosophy of mathematics, history of logic and analytic philosophy. For the ‘n-community’, one should point out his recent work on homotopical ideas in type theory.

Selected writings

On propositional truncation in dependent type theory:

On algebraic set theory:

  • Steve Awodey. Notes on algebraic set theory, Notes for lectures given at the Summer School on Topos Theory, Haute-Bodeux, Belgium. May 29 to June 5, 2005. Carnegie Mellon University Technical Report No. CMU-PHIL-170. June 2005. (pdf)

On category theory:

Early note on what came to be known as homotopy type theory:

  • Steve Awodey, Homotopy and Type Theory, grant proposal project description (pdf)

Proof that every simplicial model category in which the cofibrations are monomorphisms provides a sound model for intensional Martin-Löf type theory (i.e. including the identity types used in homotopy type theory):

Stating Awodey's conjecture:

On inductive types in homotopy type theory via homotopy-initial algebras over an endofunctor:

and analogously on higher inductive types:

On first-order set theory and categorical logic:

On natural models of homotopy type theory:

On Kripke-Joyal semantics and forcing in homotopy type theory:

On the model category structure on the category of cartesian cubical sets:

category: people

Last revised on July 28, 2023 at 10:11:33. See the history of this page for a list of all contributions to it.