When attempting to prove a theorem, not discussed in this post, I tried to give a certain set the structure of a group. After failing repeatedly, my proof attempts led me to consider a miniature version of the problem: can , the object of truth values, be given the structure of a group?

This question makes sense in 1-topos theory, in -topos theory and in HoTT/UF, where in the latter a truth value is a type with at most one element, also known as a proposition (and sometimes as an h-proposition or as a mere proposition).

The answer to the question, in all cases, turns out to be that can be given the structure of a group if and only if the topos is boolean.

Reasoning in the internal language, or the type theory, the argument is as follows.

If the topos is boolean, that is, excluded middle holds in the internal language, then trivially has precisely two group structures, and endowed with each of them gives rise to two isomorphic groups.

It is the converse that is interesting.

We use “Higgs’ Involution Theorem”, which says that every left-cancellable map is an involution, that is, .

If a group structure on is given, by Higgs’ involution
theorem we conclude that it is abelian with for every
(where it is unspecified which element of the zero element of the
group is – it can be , , or any element of ).

Now define .

Then we have the following chain of logical equivalences:

.

Hence by propositional extensionality (or univalence for propositions, in the case of HoTT/UF).

But , being a group action, is an automorphism and hence an
involution by Higgs’ theorem (or already by the above consequences of
Higgs’ theorem and direct calculation), which amounts to , and
therefore excluded middle holds.

This argument is also written here in Agda, with a weaker assumption, namely that is given the structure of a left-cancellative monoid, including a proof of Higgs Involution Theorem.

I wouldn’t be surprised if this fact is already available in the literature or the folklore. Is it?