Martin-Lof identity types in the C-systems defined by a universe category | Vladimir Voevodsky

Submitted by vladimir on Tue, 2015-05-26 06:36

Publication Type:

Journal Article

Authors:

Voevodsky, Vladimir

Source:

arXiv 1505.06446, submitted, p.1–51 (2015)

URL:

http://arxiv.org/abs/1505.06446

Weight:

6