You should start from `unit`

(which is in `Set`

) instead of `True`

(which is in `Prop`

and the reason why you have problems here, I believe). And indeed you can equip it with a fingroup type if you want (it is already a finite type in the library). Otherwise if you're just looking for any fingroup with one element, you could also use either `{perm unit}`

(the permutations of the type `unit`

with a single element) or `{unit bool}`

(the type of inversible elements (a.k.a. units) of the ring of booleans).

Raül has marked this topic as resolved.

Last updated: Jul 15 2024 at 20:02 UTC