The biequivalence of locally cartesian closed categories and Martin-Löf type theories

DOI10.1017/S0960129513000881zbMath1342.03046arXiv1112.3456OpenAlexW3104964042WikidataQ56228325 ScholiaQ56228325MaRDI QIDQ5740406

Peter Dybjer, Pierre Clairambault

Publication date: 26 July 2016

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Fibered categories (18D30) Other constructive mathematics (03F65)

Related Items (14)

Bicategories in univalent foundations ⋮ A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types ⋮ On generalized algebraic theories and categories with families ⋮ A general framework for the semantics of type theory ⋮ Towards a constructive simplicial model of Univalent Foundations ⋮ Game semantics of Martin-Löf type theory ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Modal dependent type theory and dependent right adjoints ⋮ Pointers in Recursion: Exploring the Tropics ⋮ Categories with families and first-order logic with dependent sorts ⋮ The (Pi,lambda)-structures on the C-systems defined by universe categories ⋮ Unnamed Item ⋮ Categories with Families: Unityped, Simply Typed, and Dependently Typed

Cites Work

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

This page was built for publication: The biequivalence of locally cartesian closed categories and Martin-Löf type theories