# Categories with Dependence and Semantics of Dependent Types

## TL;DR

This paper introduces a generalized categorical framework called cartesian closed categories with dependence, providing a new semantics for dependent type theories that aligns with both categorical structures and syntactic precision.

## Contribution

It extends cartesian closed categories to include dependence, supporting complex type structures like Sigma and Pi types in a strict categorical setting.

## Key findings

- Developed a new categorical semantics for dependent type theories
- Supported strict Sigma and Pi types in the new framework
- Bridged categorical models with syntactic type theories

## 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.