Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation

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

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 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?)
• Title not available (Why is that?)
• A Kripke model for simplicial sets

Cited In (1)

• 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)