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

anonymous existencebracket typesconstant endofunctionsHedberg's theoremhomotopy type theorypropositional equalitysquash typestruncation

Mathematics Subject Classification ID

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

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

(9)

• Notions of anonymous existence in Martin-Löf type theory
• Partiality, Revisited
• Homotopy theoretic models of identity types
• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• Quotienting the delay monad by weak bisimilarity
• Indexed type theories
• Eliminating dependent pattern matching without K
• Covering spaces in homotopy type theory
• Proof of the H-theorem for isolated binary gas-photon gas mixtures

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)