Functional Kan simplicial sets: non-constructivity of exponentiation

DOI10.4230/LIPICS.TYPES.2015.8zbMATH Open1434.03020OpenAlexW3087220398MaRDI QIDQ4580229FDOQ4580229

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/

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

zbMATH Keywords

constructive logicsimplicial setssemantics of simple types

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Simplicial homotopy theory
• Axiom of Choice and Complementation
• Survey article: an elementary illustrated introduction to simplicial sets
• Title not available (Why is that?)
• Algebraic models for higher categories
• Title not available (Why is that?)
• Non-constructivity in Kan simplicial sets
• A Kripke model for simplicial sets

Cited In (3)

• Exponentials of non-singular simplicial sets
• Non-constructivity in Kan simplicial sets
• Examples and cofibrant generation of effective Kan fibrations

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)