That's because ∀ {A}
is actually just a syntactic sugar for {A : _}
, which asks the compiler to fill A
's type automatically.
This doesn't work quite well with just Set
s, because you could have:
{A : Set}
{A : Set₁}
{A : Set₂}
-- etc.
And indeed, all of those are valid types in your definition. ∀
really only makes sense when the thing that follows can be unambiguously determined by its use.
For example, consider this definition:
data List (A : Set) : Set where
-- ...
map : ∀ {A B} → (A → B) → List A → List B
map = -- ...
The type of A
must be Set
, because List
only works with Set
s.
However, because it's just a sugar for {A : _}
that means it works with much more than just Set
s.
_+_ : ℕ → ℕ → ℕ
_+_ = -- ...
comm : ∀ x y → x + y ≡ y + x
comm = -- ...
Or perhaps the most common use case:
map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → List A → List B
The type of a
and b
is Level
; this is called universe polymorphism.