What is type theory (theory)?

Events / Oxford Seminar

Description

Join us to hear an account of (re-)inventing what type theory is, from a position of ignorance. Specifically the work to be discussed arose as an attempt to understand what a “coordinate free” understanding of type theory might be, and why and whether we might be interested in such a thing. In particular, the to-be-discussed framework eschews the “usual” microcosm approach of categorical type theoretic accounts in which (external) limits and colimits are used to model internal ones and the various calculi of syntax thereupon.

Optional background: Cursory experience with sheaves and type theory is likely to be useful.