Comprehension categories and the semantics of type dependency

DOI10.1016/0304-3975(93)90169-TzbMath0804.18007MaRDI QIDQ1208414

Bart Jacobs

Publication date: 16 May 1993

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

functortoposfibrationadjunctioncomprehensionclosed categoryhyperdoctrinetype dependency

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55) Categorical logic, topoi (03G30) Topoi (18B25) Fibered categories (18D30) Theories (e.g., algebraic theories), structure, and semantics (18C10)

Related Items

Towards a directed homotopy type theory, A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types, Logical systems. I: Internal calculi., Internal languages of finitely complete \((\infty , 1)\)-categories, Elimination of extensionality in Martin-Löf type theory, The Local Universes Model, A general framework for the semantics of type theory, On the ∞$\infty$‐topos semantics of homotopy type theory, Semantical analysis of contextual types, Universal properties for universal types in bifibrational parametricity, Comprehensive factorisation systems, Revisiting the categorical interpretation of dependent type theory, Combinatorial structure of type dependency, Displayed Categories, Unnamed Item, The simplicial model of univalent foundations (after Voevodsky), Comprehensive Parametric Polymorphism: Categorical Models and Type Theory, Two-dimensional models of type theory, Structural induction and coinduction in a fibrational setting, Equilogical spaces, CATEGORICAL MODEL CONSTRUCTION FOR PROVING SYNTACTIC PROPERTIES, Univalence and completeness of Segal objects, MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Alpha conversion, conditions on variables and categorical logic
• Generalized algebraic theories and contextual categories
• On the syntax of Martin-Löf's type theories
• A small complete category
• A compositional proof system on a category of labelled transition systems
• Locally cartesian closed categories and type theory
• Fibered categories and the foundations of naive category theory
• Constructive natural deduction and its ‘ω-set’ interpretation
• A category-theoretic account of program modules
• Dictoses
• Aspects of topoi: Corrigenda and acknowledgements