Generalizations of Hedberg's theorem

DOI10.1007/978-3-642-38946-7_14MaRDI QIDQ5300901zbMATH OpenOpenAlexWikidataFDO

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

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)

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 -groupoid laws using parametricity theory
• Homotopy theoretic models of identity types

Cited in

(8)

• Eliminating dependent pattern matching without K
• Partiality, Revisited
• Proof of the H-theorem for isolated binary gas-photon gas mixtures
• Covering spaces in homotopy type theory
• Indexed type theories
• Quotienting the delay monad by weak bisimilarity
• Notions of anonymous existence in Martin-Löf type theory
• Homotopy theoretic models of identity types

Describes a project that uses

Uses Software

• Agda
• Coq

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)