2017/04/16 by Yamada, Norihiro
#Category Theory (math.CT) #FOS: Computer and information sciences #FOS: Mathematics #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1704.04747
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.