Locally cartesian closed categories without chosen constructions

zbMATH Open1163.18003MaRDI QIDQ5454624FDOQ5454624

Authors: Erik Palmgren 

Publication date: 31 March 2008

Full work available at URL: https://eudml.org/doc/129995

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

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

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)

Cited In (3)

• Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets
• Univalence in locally Cartesian closed categories
• Title not available (Why is that?)

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)