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?

### Like this:

Like Loading...

*Related*

Update: none of the topos theorists we asked, including Peter Johnstone, were aware of the fact that the object of truth values can be a group only in a boolean topos.