What does \forall (∀) actually mean in a signature?

Question

From the bits and pieces of information I gathered about agda I'd (apparently erroneously) concluded that `∀ {A}` was equivalent to `{A : Set}`. Now I noticed that ``` flip : ∀ {A B C} -> (A -> B -> C) -> (B -> A -> C) ``` is invalid (something about Set\omega which in turn seems to be some internal something, but ``` flip : {A B C : Set} -> (A -> B -> C) -> (B -> A -> C) ``` is fine. Can anyone clear this up for me?

Accepted Answer

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.

What does \forall (∀) actually mean in a signature?

Solution

Problem