Locally cartesian closed categories without chosen constructions

MaRDI QIDQ5454624zbMATH OpenFDO

Authors Erik Palmgren

Publication date 31 March 2008

Full work available at URL https://eudml.org/doc/129995, http://www.emis.de/journals/TAC/volumes/20/1/20-01abs.html

IPFS File on IPFS (Hint: this is only the Hash - if you get a timeout, this file is not available on our server.)

Mathematics Subject Classification ID

Categories admitting limits (complete categories), functors preserving limits, completions (18A35) Adjoint functors (universal constructions, reflective subcategories, Kan extensions, etc.) (18A40) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)

Recommendations

• Functional completeness of the free locally Cartesian closed category and interpretations of Martin-Löf's theory of dependent types
• The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
• Locally cartesian closed categories and type theory
• Avoiding the axiom of choice in general category theory
• scientific article; zbMATH DE number 2079044

Cited in

(3)

• Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets
• Univalence in locally Cartesian closed categories
• scientific article; zbMATH DE number 25966 (Why is no real title available?)

This page was built for publication: Locally cartesian closed categories without chosen constructions

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