A general framework for the semantics of type theory
From MaRDI portal
Publication:6149910
DOI10.1017/s0960129523000208arXiv1904.04097MaRDI QIDQ6149910
Publication date: 5 March 2024
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1904.04097
logical frameworkdependent type theorynatural modelcategory with familiesrepresentable maprepresentable map category
Cites Work
- Fibred 2-categories and bicategories
- Cartesianness: topological spaces, uniform spaces, and affine schemes
- Comprehension categories and the semantics of type dependency
- Categorical logic and type theory
- Some properties of Fib as a fibred \(2\)-category
- The homotopy theory of type theories
- The universal exponentiable arrow
- Internal languages of finitely complete \((\infty , 1)\)-categories
- Lokal präsentierbare Kategorien. (Locally presentable categories)
- A judgmental reconstruction of modal logic
- Natural models of homotopy type theory
- Discrete Generalised Polynomial Functors
- Locally cartesian closed categories and type theory
- HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
- A framework for defining logics
- A construction of certain weak colimits and an exactness property of the 2-category of categories
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- Higher Categories and Homotopical Algebra
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory
- Internal type theory
- Model structures on categories of models of type theories
- Modal dependent type theory and dependent right adjoints
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Higher Topos Theory (AM-170)
- The biequivalence of locally cartesian closed categories and Martin-Löf type theories
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item