Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation

DOI10.4230/LIPIcs.TYPES.2015.8zbMath1434.03020OpenAlexW3087220398MaRDI QIDQ4580229

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

simplicial setsconstructive logicsemantics of simple types

Mathematics Subject Classification ID

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

Uses Software

• Coq

Cites Work

• Survey article: an elementary illustrated introduction to simplicial sets
• Algebraic models for higher categories
• A Kripke model for simplicial sets
• Axiom of Choice and Complementation
• Simplicial homotopy theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation