Categories with dependent arrows

TL;DR

This paper develops a categorical framework for dependent functions using categories with family-arrows and dependent arrows, providing a foundational and independent approach from the Sigma-construction.

Contribution

It introduces the concepts of $$-categories, $,\Sigma$-categories, and $ ext{di}$-categories, establishing their relationships and canonical embeddings, advancing the categorical understanding of dependent types.

Findings

Every $(,\Sigma)$-category is a $ ext{di}$-category in a canonical way.

The notion of Sigma-objects in $ ext{di}$-categories is influenced by dependent arrows.

The framework generalizes type-category concepts independently of the Sigma-construction.

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