Functional Kan simplicial sets: non-constructivity of exponentiation

DOI10.4230/LIPICS.TYPES.2015.8MaRDI QIDQ4580229zbMATH OpenOpenAlexFDO

Authors Erik Parmann

Publication date 13 August 2018

Full work available at URL http://drops.dagstuhl.de/opus/volltexte/2018/8478/pdf/LIPIcs-TYPES-2015-8.pdf/

zbMATH Keywords

constructive logicsemantics of simple typessimplicial sets

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Metamathematics of constructive systems (03F50) Categorical logic, topoi (03G30) Simplicial sets, simplicial objects (18N50) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Non-constructivity in Kan simplicial sets
• Another approach to the Kan-Quillen model structure
• Effective Kan fibrations in simplicial sets
• The simplicial model of univalent foundations (after Voevodsky)
• A dependently-typed construction of semi-simplicial types

Cites work

• A Kripke model for simplicial sets
• Algebraic models for higher categories
• Axiom of Choice and Complementation
• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• scientific article; zbMATH DE number 3124495 (Why is no real title available?)
• scientific article; zbMATH DE number 206022 (Why is no real title available?)
• scientific article; zbMATH DE number 3222098 (Why is no real title available?)
• Non-constructivity in Kan simplicial sets
• Simplicial homotopy theory
• Survey article: an elementary illustrated introduction to simplicial sets

Cited in

(5)

• Exponentials of non-singular simplicial sets
• Non-constructivity in Kan simplicial sets
• The Constructive Kan–Quillen Model Structure: Two New Proofs
• Examples and cofibrant generation of effective Kan fibrations
• The equivariant model structure on cartesian cubical sets

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Functional Kan simplicial sets: non-constructivity of exponentiation

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