Type theories in category theory

TL;DR

This paper introduces foundational categorical concepts relevant to type theorists, providing detailed definitions, proofs, and discussions to facilitate understanding of the interpretation of type formers in category theory.

Contribution

It offers a comprehensive, accessible overview of categorical notions related to type theories, with detailed proofs and discussions that are useful as a reference for researchers.

Findings

Categorical interpretations of common type formers are discussed.

Includes detailed proofs and diagrams for key categorical concepts.

Provides a friendly, reference-oriented presentation for type theorists.

Abstract

We introduce basic notions in category theory to type theorists, including comprehension categories, categories with attributes, contextual categories, type categories, and categories with families along with additional discussions that are not very closely related to type theories by listing definitions, lemmata (with detailed, diagram-rich proofs), and remarks. By doing so, this introduction becomes more friendly as a referential material to be read in random order (instead of from the beginning to the end). In the end, we list some mistakes made in the early versions of this introduction. The interpretation of common type formers in dependent type theories are discussed based on existing categorical constructions instead of mechanically derived from their type theoretical definition. Non-dependent type formers include unit, products (as fiber products), and functions (as fiber exponents), and dependent ones include sigma types, extensional equalities (as equalizers), pi types, and the universe of (all) propositions (as the subobject classifier).