English

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 \f\f-category. A (\f,Σ)(\f, \Sigma)-category is a \f\f-category with Sigma-objects, where a (\f,Σ)(\f, \Sigma)-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 \di\di-categories, and we show that every (\f,Σ)(\f, \Sigma)-category is a \di\di-category in a canonical way. The notion of a Sigma-object in a \di\di-Category is affected by the existence of dependent arrows, and we show that every (\f,Σ)(\f, \Sigma)-category is a (\di,Σ)(\di, \Sigma)-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

R2 v1 2026-06-28T09:34:16.525Z