Algebraic Type Theory and Universe Hierarchies
Logic in Computer Science
2019-02-26 v1 Logic
Abstract
It is commonly believed that algebraic notions of type theory support only universes \`a la Tarski, and that universes \`a 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 \`a la Russell. To demonstrate the power of algebraic techniques, we sketch a purely algebraic proof of canonicity for Martin-L\"of Type Theory with universes, dependent function types, and a base type with two constants.
Keywords
Cite
@article{arxiv.1902.08848,
title = {Algebraic Type Theory and Universe Hierarchies},
author = {Jonathan Sterling},
journal= {arXiv preprint arXiv:1902.08848},
year = {2019}
}