module
Σ
where
A
:
Set₁
A
=
Set