Comprehension categories and the semantics of type dependency
type: Item
instance of: scholarly article
title: Comprehension categories and the semantics of type dependency
zbMATH Open document ID: 0804.18007
DOI: 10.1016/0304-3975(93)90169-T
author: Bart Jacobs
published in: Theoretical Computer Science
publication date: 1993-05-16T00:00:00Z
review text: A comprehension category is a functor \({\mathcal P} : \mathbb{E} \to \mathbb{B}^ \to\) such that (i) \(cod \circ {\mathcal P} : \mathbb{E} \to \mathbb{B}\) is a fibration, and (ii) \(f\) is cartesian in \(\mathbb{E}\) implies that \({\mathcal P}f\) is a pullback in \(\mathbb{B}\). Here \(\mathbb{B}^ \to\) is the arrow category of \(\mathbb{B}\), and \(cod : \mathbb{B}^{\to}\to \mathbb{B}\) is the codomain functor. The author starts with a presentation of the basic facts about fibrations and fibered adjunctions due to A. Grothendieck and J. Bénabou. The paper is mainly devoted to the discussion of numerous examples of comprehension categories. It is shown that many categorical structures introduced by various authors to describe type dependency are particular cases of the general notion of a comprehension category. Examples include, among others, term model, display-map categories, topos comprehension, categories with attributes, Ehrhard's \(D\)-categories, family models, Lawvere's hyperdoctrines, Pavlović's comprehension. Closed comprehension categories are also discussed.
Mathematics Subject Classification ID: 18D30
Mathematics Subject Classification ID: 68Q55
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 68N15
Mathematics Subject Classification ID: 18B25
Mathematics Subject Classification ID: 18C10
zbMATH DE Number: 166426
zbMATH Keywords: adjunction
zbMATH Keywords: closed category
zbMATH Keywords: comprehension
zbMATH Keywords: fibration
zbMATH Keywords: functor
zbMATH Keywords: hyperdoctrine
zbMATH Keywords: topos
zbMATH Keywords: type dependency
describes a project that uses: Automath
reviewed by: Antoni Wiweger
MaRDI profile type: Publication
cites work: Q3682648
cites work: Fibered categories and the foundations of naive category theory
cites work: Generalized algebraic theories and contextual categories
cites work: Q3785893
cites work: Alpha conversion, conditions on variables and categorical logic
cites work: Dictoses
cites work: Aspects of topoi: Corrigenda and acknowledgements
cites work: Q5507553
cites work: Q5586462
cites work: Q5655486
cites work: A small complete category
cites work: Q5752573
cites work: Q4282579
cites work: Q4145861
cites work: Q5642701
cites work: Q5639839
cites work: Q3688389
cites work: A category-theoretic account of program modules
cites work: Constructive natural deduction and its ‘ω-set’ interpretation
cites work: Q4170869
cites work: Q3786612
cites work: Locally cartesian closed categories and type theory
cites work: Q4733863
cites work: On the syntax of Martin-Löf's type theories
cites work: A compositional proof system on a category of labelled transition systems
description: scientific article; zbMATH DE number 166426