Why can't (Set -> Set) have type Set?

Question

In Agda, the type of a forall is determined in such a way that the following all have type Set1 (where Set1 is the type of Set and A has type Set):

Set → A
A → Set
Set → Set

However, the following has type Set:

A → A

I understand that if Set had type Set, there would be contradictions, but I'm failing to see how, if any of the three terms above had type Set, we would have contradictions. Can those be used to prove False? Can they be used to show that Set : Set?

Answer 1

It is clear that Set : Set would cause a contradiction, such as Russell's paradox.

Now consider () -> Set where () is a unit type. This is clearly isomorphic to Set. So if () -> Set : Set then also Set : Set. In fact, if for any inhabited A we had A -> Set : Set then we could wrap Set into A -> Set using a constant function:

wrap1 : {A : Set} -> Set -> (A -> Set)
wrap1 v = \_ -> v

and get the value whenever needed as

unwrap1 : {A : Set}(anyInhabitant : A) -> (A -> Set) -> Set
unwrap1 anyInhabitant f = f anyInhabitant

So we could reconstruct Russell's paradox just as if we had Set : Set.

---

The same applies for Set -> Set, we could wrap Set into Set -> Set:

data Void : Set where

unwrap2 : (Set -> Set) -> Set
unwrap2 f = f Void

wrap2 : Set -> (Set -> Set)
wrap2 v = \_ -> v

Here we could use any type of Set instead of Void.

---

I'm not sure how to do something similar with Set -> A, but intuitively this seems to be even more problematic type than the other ones, maybe someone else will know.

Answer 2

I think the best way to understand this is to consider what these things are like as set-theoretic sets, as opposed to as Agda Set. suppose you have A = {a,b,c}. An example of a function f : A → A is a set of pairs, let's say f = { (a,a) , (b,b) , (c,c) } that satisfies some properties that don't matter for this discussion. That is to say, f's elements are the same sort of thing that A's elements are -- they're just values, or pairs of values, nothing too "big".

Now consider the a function F : A → Set. It too is a set of pairs, but its pairs look different: F = { (a,A) , (b,Nat) , (c,Bool) } lets say. The first element of each pair is just an element of A, so it's pretty simple, but the second element of each pair is a Set! That is, the second element is itself a "big" sort of thing. So A → Set couldn't possibly be set, because if it were, then we should be able to have some G : A → Set that looks like G = { (a,G) , ... }. As soon as we can have this, we can get Russell's paradox. So we say A → Set : Set1 instead.

This also addresses the issue of whether or not Set → A should also be in Set1 instead of Set, because the functions in Set → A are just like the functions in A → Set, except that the As are on the right, and the Sets are on the left, of the pairs.