References & Citations
Computer Science > Logic in Computer Science
Title: Type theories in category theory
(Submitted on 28 Jul 2021 (v1), last revised 4 Apr 2022 (this version, v5))
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).
Submission history
From: Tesla Zhang [view email][v1] Wed, 28 Jul 2021 09:54:39 GMT (50kb)
[v2] Tue, 1 Mar 2022 09:52:22 GMT (51kb)
[v3] Tue, 22 Mar 2022 06:29:29 GMT (58kb)
[v4] Mon, 28 Mar 2022 04:19:58 GMT (60kb)
[v5] Mon, 4 Apr 2022 11:43:08 GMT (62kb)
Link back to: arXiv, form interface, contact.