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

extensional type theorylocally Cartesian closed categoriesundecidability

Mathematics Subject Classification ID

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

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

(12)

• Undecidability of the free adjoint construction
• Three extensional models of type theory
• A coherence theorem for Martin-Löf's type theory
• Functional completeness of the free locally Cartesian closed category and interpretations of Martin-Löf's theory of dependent types
• Categories with families: unityped, simply typed, and dependently typed
• On generalized algebraic theories and categories with families
• Cubical syntax for reflection-free extensional equality
• Modal dependent type theory and dependent right adjoints
• Undecidability of equality in the free locally Cartesian closed category
• Displayed type theory and semi-simplicial types
• Toward a geometry for syntax
• Tableaux for automated reasoning in dependently-typed higher-order logic

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)