Is there a way to mention the type of the powerset of a set?

For example, type of set of booleans is `[set bool]`

.

```
Check [set true]: {set bool}.
```

Is there a way to express the type of sets whose elements are `[set bool]`

?

Would this be a right way?

```
Check [set [set true]]: {set {set bool}}.
```

Technically, the type of sets of booleans is `{set bool}`

.

Regarding the powerset of a set, I assume you would like to have `A : {set bool}`

and be able to write `X : {set A}`

. This is not possible as of now because we would need a structure of `finType`

on `A`

, which we can not declare (afaict).

Regarding the type of sets whose elements are of type `{set bool}`

, it is indeed `{set {set bool}}`

.

I just stumbled upon `powerset`

, which might do what you want.

Last updated: Jul 15 2024 at 20:02 UTC