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
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)
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