Categories with Families: Unityped, Simply Typed, and Dependently Typed

DOI10.1007/978-3-030-66545-6_5zbMath1478.18001arXiv1904.00827OpenAlexW3176769887MaRDI QIDQ5014596

Peter Dybjer, Pierre Clairambault, Simon Castellan

Publication date: 8 December 2021

Published in: Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1904.00827

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Categorical logic, topoi (03G30) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Research exposition (monographs, survey articles) pertaining to category theory (18-02)

Related Items (1)

On generalized algebraic theories and categories with families

Cites Work

• Generalized algebraic theories and contextual categories
• Categorical logic and type theory
• Revisiting the categorical interpretation of dependent type theory
• The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads
• Game Semantics and Normalization by Evaluation
• The Local Universes Model
• The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
• Natural models of homotopy type theory
• Discrete Generalised Polynomial Functors
• Locally cartesian closed categories and type theory
• Fibered categories and the foundations of naive category theory
• Categorical combinators
• Internal type theory
• Categorical structures for type theory in univalent foundations
• Polynomials in categories with pullbacks
• 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
• Unnamed Item
• Unnamed Item

This page was built for publication: Categories with Families: Unityped, Simply Typed, and Dependently Typed