Notions of anonymous existence in Martin-Löf type theory

DOI10.23638/LMCS-13(1:15)2017MaRDI QIDQ2980980zbMATH OpenFDO

Authors Nicolai Kraus, Martín Escardo, Thierry Coquand, Thorsten Altenkirch

Publication date 8 May 2017

Full work available at URL https://arxiv.org/abs/1610.03346

zbMATH Keywords

truncationfactorizationhomotopy type theorycoherence conditionsanonymous existencebracket typesHedberg's theoremsquash typesweakly constant functions

Mathematics Subject Classification ID

Logic in computer science (03B70) Categorical logic, topoi (03G30) Functional programming and lambda calculus (68N18)

Recommendations

• Generalizations of Hedberg's theorem
• A coherence theorem for Martin-Löf's type theory
• scientific article; zbMATH DE number 6694181
• Martin-Löf complexes
• Idempotents in intensional type theory

Cites work

• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• scientific article; zbMATH DE number 1302061 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• A coherence theorem for Martin-Löf's type theory
• A course in constructive algebra
• Axiom of Choice and Complementation
• Generalizations of Hedberg's theorem
• Homotopy theoretic models of identity types
• Notions of anonymous existence in Martin-Löf type theory
• Proof-relevance of families of setoids and identity in type theory
• Propositions as [Types]
• The World's simplest axiom of choice fails
• The general universal property of the propositional truncation

Cited in

(10)

• Univalent categories of modules
• Type theory based semantic verification for service composition in cloud computing environments
• Generalizations of Hedberg's theorem
• The Scott model of PCF in univalent type theory
• Extensional constructive real analysis via locators
• Notions of anonymous existence in Martin-Löf type theory
• The justification of identity elimination in Martin-Löf's type theory
• Type-theoretic approaches to ordinals
• On Small Types in Univalent Foundations
• Idempotents in intensional type theory

Describes a project that uses

Uses Software

• GitHub

This page was built for publication: Notions of anonymous existence in Martin-Löf type theory

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