18 citations · 20 across the 3 of their papers we have counts for
4 papers
Toward the effective 2-topos
Steve Awodey, Jacopo Emmenegger
A candidate for the effective 2-topos is proposed and shown to include the effective 1-topos as its subcategory of 0-types.
On Hofmann-Streicher universes
Steve Awodey
We have another look at the construction by Hofmann and Streicher of a universe for the interpretation of Martin-Löf type theory in a presheaf category $\psh{\C…
Impredicative Encodings of (Higher) Inductive Types
Steve Awodey, Jonas Frey, Sam Speight
Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and…
Natural models of homotopy type theory
Steve Awodey
The notion of a natural model of type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly with the…