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.
A textbook account can be found in the HoTT book.
The theorem was first published in
Hedberg, Michael. 1998. ‘A Coherence Theorem for Martin-Löf’s Type Theory’. Journal of Functional Programming 8 (4): 413–36. https://doi.org/10.1017/S0956796898003153. [pdf]
@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},
}