scientific article; zbMATH DE number 6816943

DOI10.23638/LMCS-13(4:22)2017MaRDI QIDQ4596801zbMATH OpenFDO

Authors Simon Castellan, Pierre Clairambault, Peter Dybjer

Publication date 11 December 2017

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

zbMATH Keywords

undecidabilitylocally Cartesian closed categoriesextensional type theory

Mathematics Subject Classification ID

Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Undecidability and degrees of sets of sentences (03D35) Type theory (03B38)

Recommendations

• Undecidability of equality in the free locally Cartesian closed category
• Univalence in locally Cartesian closed categories
• A note on Russell's paradox in locally Cartesian closed categories
• The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
• The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
• On locally finite varieties with undecidable equational theory.
• On the unification problem for Cartesian closed categories
• Coherence in Cartesian closed categories and the generality of proofs
• Functional completeness of the free locally Cartesian closed category and interpretations of Martin-Löf's theory of dependent types
• A note on inconsistencies caused by fixpoints in a cartesian closed category

Cited in

(7)

• Three extensional models of type theory
• Undecidability of equality in the free locally Cartesian closed category
• Undecidability of the free adjoint construction
• scientific article; zbMATH DE number 7559297 (Why is no real title available?)
• Modal dependent type theory and dependent right adjoints
• Categories with families: unityped, simply typed, and dependently typed
• On generalized algebraic theories and categories with families

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4596801)