Categories with Dependence and Semantics of Dependent Types
Reviewed by Pith T0 review T1 audit T2 compute T3 formal T4 kernel pith:ZWLBZ7XDrecord.jsonopen to challenge →
classification
math.CT
cs.LO
keywords
categoriescartesiancloseddependencedependentsemanticsstrictcalled
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.