Categories with Dependence and Semantics of Dependent Types
Category Theory
2019-02-26 v3 Logic in Computer Science
Abstract
The present paper gives a generalization of cartesian closed categories, called cartesian closed categories with dependence, whose strict version induces categories with families that support 1-, Sigma- and Pi-types in the strict sense. Consequently, we have obtained a new semantics of dependent type theories that is both categorical and true-to-syntax.
Keywords
Cite
@article{arxiv.1704.04747,
title = {Categories with Dependence and Semantics of Dependent Types},
author = {Norihiro Yamada},
journal= {arXiv preprint arXiv:1704.04747},
year = {2019}
}