Generalizations of Hedberg’s Theorem

DOI10.1007/978-3-642-38946-7_14zbMath1433.03032OpenAlexW161151979WikidataQ61583728 ScholiaQ61583728MaRDI QIDQ5300901

Thierry Coquand, Nicolai Kraus, Thorsten Altenkirch, Martín Hötzel Escardó

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)

Related Items (5)

Unnamed Item ⋮ Quotienting the delay monad by weak bisimilarity ⋮ Eliminating dependent pattern matching without K ⋮ Partiality, Revisited ⋮ Indexed type theories

Uses Software

• Coq
• Agda

This page was built for publication: Generalizations of Hedberg’s Theorem