In type theory and constructive mathematics, Hedberg's theorem says:
A type with decideable equality is automatically a set.
But coming at it from a classical viewpoint, I don't understand how this could be true. If I understand correctly, the word "type" in this context basically means "$\infty$-groupoid." Okay, so consider the delooping $G$ of the group $\mathbb{Z}/2\mathbb{Z}.$ It follows that $G$ is the groupoid with one object and two automorphisms. Since there's only one object, equality of objects is decidable. And since there exist parallel morphisms that aren't equal, $G$ is not a set.
What am I not understanding here?
The point is continuity: In the homotopy-type-theoretic context, decidable equality for a type $X$ means that the type $\Pi_{x,y : X} (x=_Xy)\vee \neg(x=_Xy)$ is inhabited, so you're requested to provide - in a continuous manner as regards to the topological interpretation (only) - either a path between $x$ and $y$ or a proof that such cannot exist. If you're working with a connected type, i.e. $\Pi_{x,y:X} \|x=_Xy\|$ is inhabited, then this is equivalent to giving an inhabitant of $\Pi_{x,y : X} (x=_Xy)$, which however is the definition of $X$ being a $-1$-type / proposition.
If you follow the naive argument, you'll also see the flaw: So in $X=B({\mathbb Z}/2{\mathbb Z})$, there's only one object, say $\ast$, and for that object we'd like to pick say the constant path $c_\ast$ as a proof of $\ast=_X\ast$. But now, we move from $\ast$ to $\ast$ in the left argument of $=_X$ via the unique nontrivial loop, say $\gamma$, and continuity would then force us to assign $\gamma\cdot c_\ast=\gamma$ to $\ast$ instead - contradiction.