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.
On propositional truncation in dependent type theory:
On category theory:
Early note on what came to be known as homotopy type theory:
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:
Steve Awodey, Nicola Gambino, Kristina Sojakova, Inductive types in homotopy type theory, LICS’12: (2012) 95–104 [arXiv:1201.3898, doi:10.1109/LICS.2012.21, Coq code]
Exposition:
Steve Awodey, Inductive types in HoTT (Jan 2012) [blog post]
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:
Last revised on July 12, 2024 at 22:11:50. See the history of this page for a list of all contributions to it.