What am I not understanding about Hedberg's theorem? 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?
 A: 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.
A: It is not possible to show that $B \Bbb Z_2$ has decidable equality because it simply isn't true. Just because there is one point doesn't mean there is decidable equality.
To see why this is, try the simpler example $S^1$ (or $B \Bbb Z$ if you like). It too has one point. Let us attempt to prove that $S^1$ has decidable equality to see what goes wrong.
We wish to construct a term with the following type:
$$\prod_{x,y : S^1}(x = y) + ¬(x=y)$$
Given $x : S^1$, we need to prove:
$$ \prod_{y : S^1}(x = y) + ¬(x=y) $$
Applying $S^1$-induction on $y$, we need to show the following:
$$p : (x = \mathsf{base})+¬(x =\mathsf{base})$$
$$q: \mathsf{transport}_P(\mathsf{loop}, p)=p$$
Where $P : S^1 \to \mathcal{U}$ is defined to be $$ \lambda y.(x=y)+¬(x=y)$$
Why can we do this? Well because this is exactly what $S^1$-induction gives. It says: I can prove $\prod_{y : S^1} P(y)$ if you give me the data $p$ and $q$. So what's left is to construct $p$ and $q$.
Working on $q$, we see that we have a $\mathsf{transport}$ over a sum (coproduct) type. In section 2.12 (just before 2.13) of the HoTT book, it is shown how transport acts over a "sum" of type families. So we need to consider two cases: if $p$ comes from the left or if $p$ comes from the right.
Focusing on the first, we see that we want to prove:
$$\mathsf{inl} \left( \mathsf{transport}_{\lambda y .(x=y)}(\mathsf{loop}, p') \right)= p\quad (\equiv \mathsf{inl}(p'))$$
where $p'$ comes from $p \equiv \mathsf{inl}(p')$. By applying $\mathsf{ap_{\mathsf{inl}}}$, we see that we need
$$ \mathsf{transport}_{\lambda y .(x=y)}(\mathsf{loop}, p') = p'$$
Now in Lemma 2.11.2 of the HoTT book, we have transports over identity types characterised. This gives us
$$ p' \cdot \mathsf{loop} = p' $$
Here is where we reach a problem. No matter what $p'$ (by extension $p$) we could of constructed, it would have to satisfy the above. We know that $\mathsf{loop}$ is non-trivial, thus we will have much trouble constructing such a $p'$.
What we have shown isn't a proof of anything per se, but rather a demonstration. To make this a proof, we would need to formally show that assuming decidable equality on the circle leads to a contradiction. The argument is probably similar.
Just because a type "has one point" doesn't mean it has decidable equality. We could construct a similar answer for $B \Bbb Z_2$ but the induction principle for classifying spaces is a bit more complicated.
I don't know what Hanno is talking about. 
