[FOM] Constructive Group Theory

[T.Forster at dpmms.cam.ac.uk]

Dear Dr Drago,

Please forgive me writing to you out of the blue like this, but your name 
came up in a google search on the above topic. I have a medium-term project 
to understand the constructive version of Quine's NF, and in the course of 
this i am moved to investigate the symmetric group on the universe, which 
is of course a set in NF. I have a feeling that constructive NF ought not 
to be able to prove the existence of any nontrivial permuations unless 
excluded middle holds - or at least that there is a weaker result of that 
nature to be had. This has caused me to consider the group of permutations 
that are not-not equal to the identity, which is of course a normal 
subgroup of Symm(V).

But less of that! Is there a good place to start reading about constructive 
group theory?

       yours

         Thomas Forster