Categories with dependent arrows
Category Theory
2023-03-28 v1 Logic
Abstract
We present an abstract, categorical formulation of dependent functions in a fundamental manner and independently from the Sigma-construction. For that, we define first the notion of a category with family-arrows, or a -category. A -category is a -category with Sigma-objects, where a -category with a terminal object is exactly a type-category of Pitts, or a category with attributes of Cartmell. We introduce categories with dependent arrows, or -categories, and we show that every -category is a -category in a canonical way. The notion of a Sigma-object in a -Category is affected by the existence of dependent arrows, and we show that every -category is a -category in a canonical way.
Keywords
Cite
@article{arxiv.2303.14754,
title = {Categories with dependent arrows},
author = {Iosif Petrakis},
journal= {arXiv preprint arXiv:2303.14754},
year = {2023}
}
Comments
20 pages