A general framework for the semantics of type theory

DOI10.1017/s0960129523000208arXiv1904.04097MaRDI QIDQ6149910

Taichi Uemura

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

zbMATH Keywords

logical frameworkdependent type theorynatural modelcategory with familiesrepresentable maprepresentable map category

Mathematics Subject Classification ID

Computer science (68-XX)

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