Hedberg's theorem

In the homotopical reading of type theory, Hedberg's theorem asserts that any type that has decidable equality is a set, i.e. has no higher-dimensional content.

References

• A textbook account can be found in the HoTT book.

• The theorem was first published in

BibTeX

@article{hedberg_1998,
	title = {A coherence theorem for {Martin}-{Löf}'s type theory},
	volume = {8},
	doi = {10.1017/S0956796898003153},
	number = {4},
	journal = {Journal of Functional Programming},
	author = {Hedberg, Michael},
	month = jul,
	year = {1998},
	pages = {413--436},
}