scientific article; zbMATH DE number 6816943

DOI10.23638/LMCS-13(4:22)2017zbMATH Open1433.03028arXiv1504.03995MaRDI QIDQ4596801FDOQ4596801

Authors: Simon Castellan, Pierre Clairambault, Peter Dybjer 

Publication date: 11 December 2017

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

Title of this publication is not available (Why is that?)

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

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)

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
• Title not available (Why is that?)
• 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)