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: Oct 13 2024 at 01:02 UTC