The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories

DOI10.1007/978-3-642-21691-6_10zbMath1331.03045OpenAlexW2027614742MaRDI QIDQ3007659

Peter Dybjer, Pierre Clairambault

Publication date: 17 June 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-21691-6_10

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)

Related Items (11)

A constructive manifestation of the Kleene-Kreisel continuous functionals ⋮ Cubical methods in homotopy type theory and univalent foundations ⋮ Data Types with Symmetries and Polynomial Functors over Groupoids ⋮ An interpretation of dependent type theory in a model category of locally cartesian closed categories ⋮ On generalized algebraic theories and categories with families ⋮ Polynomial functors and polynomial monads ⋮ Revisiting the categorical interpretation of dependent type theory ⋮ The homotopy theory of type theories ⋮ Model structures on categories of models of type theories ⋮ Dependent Types and Fibred Computational Effects ⋮ Categories with Families: Unityped, Simply Typed, and Dependently Typed

Cites Work

• Generalized algebraic theories and contextual categories
• Locally cartesian closed categories and type theory
• Fibered categories and the foundations of naive category theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories