Contextual Categories and Categorical Semantics of Dependent Types
Thomas Streicher · Birkhäuser Boston eBooks · 1991
By 1978, John Cartmell has introduced the notion of a contextual category in his Ph.D.Thesis on Generalised Algebraic Theories and Contextual Categories [Cartl], part of which has been published as [Cart2]. We give a detailed exposition of his work on contextual categories in order to be able to explain our notion of categorical model for the Calculus of Constructions which is based on Cartmell’s notion of contextual category. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.