A 2-categorical analysis of context comprehension

MaRDI QIDQ6634618

Jacopo Emmenegger, Greta Coraglia

Publication date: 8 November 2024

Published in: Theory and Applications of Categories (Search for Journal in Brave)

zbMATH Keywords

coalgebradependent type theory2-category theorystructure-semantics adjunctioncategory with familiescomprehension category

Mathematics Subject Classification ID

Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45) 2-dimensional monad theory (18N15) Formal category theory (18D70)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Homotopy theory in general categories
• Generalized algebraic theories and contextual categories
• Comprehension categories and the semantics of type dependency
• Categorical logic and type theory
• Categories with families and first-order logic with dependent sorts
• Adjoint functors and triples
• Kan extensions in enriched category theory
• The formal theory of monads
• Natural models of homotopy type theory
• Internal type theory
• A category-theoretic account of program modules
• Every Standard Construction is Induced by a Pair of Adjoint Functors
• Abstract homotopy theory and generalized sheaf cohomology
• The biequivalence of locally cartesian closed categories and Martin-Löf type theories
• A general framework for the semantics of type theory

This page was built for publication: A 2-categorical analysis of context comprehension

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6634618)