Generalizations of Hedberg's theorem

DOI10.1007/978-3-642-38946-7_14zbMATH Open1433.03032OpenAlexW161151979WikidataQ61583728 ScholiaQ61583728MaRDI QIDQ5300901FDOQ5300901

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

Publication date: 28 June 2013

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-38946-7_14

Recommendations

• Notions of anonymous existence in Martin-Löf type theory
• Martin Hofmann’s contributions to type theory: Groupoids and univalence
• scientific article; zbMATH DE number 1302059
• Canonicity of weak \(\omega\)-groupoid laws using parametricity theory
• Homotopy theoretic models of identity types

zbMATH Keywords

truncationhomotopy type theoryanonymous existencebracket typesHedberg's theoremsquash typespropositional equalityconstant endofunctions

Mathematics Subject Classification ID

Topological categories, foundations of homotopy theory (55U40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Type theory (03B38)

Cited In (7)

• Eliminating dependent pattern matching without K
• Title not available (Why is that?)
• Partiality, Revisited
• Proof of the H-theorem for isolated binary gas-photon gas mixtures
• Indexed type theories
• Quotienting the delay monad by weak bisimilarity
• Homotopy theoretic models of identity types

Uses Software

• Coq
• Agda

This page was built for publication: Generalizations of Hedberg's theorem

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