Algebraic Type Theory and Universe Hierarchies

02/23/2019
by   Jonathan Sterling, et al.
0

It is commonly believed that algebraic notions of type theory support only universes à la Tarski, and that universes à la Russell must be removed by elaboration. We clarify the state of affairs, recalling the details of Cartmell's discipline of _generalized algebraic theory_, showing how to formulate an algebraic version of Coquand's cumulative cwfs with universes à la Russell. To demonstrate the power of algebraic techniques, we sketch a purely algebraic proof of canonicity for Martin-Löf Type Theory with universes, dependent function types, and a base type with two constants.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset