[Agda] How to formalize 'there exists a set' phrase?

[Dan Doel]

On Friday 09 July 2010 11:59:57 am Rypacek, Ondrej wrote:
> On Jul 7, 2010, at 11:19 PM, Rypacek, Ondrej wrote:
> >> Subsets of A can be interpreted as functions A → Set:
> But A -> Set doesn't fit into Set , for A : Set . It is an ZF axiom .
> Or is this one inconsistent intuitionistically ?
> Or perhaps that's where quotients would help to make things precise and fit
> the powerset of A : Set a into Set ?

It isn't inconsistent, as far as I know. What it is, is impredicative. One of 
the problems I've kept at the back of my mind for a while is formalizing 
something like ZF in Agda, but I haven't succeeded so far. You can do it in 
Coq, however. One way is like:

  data Z : Set where
    sup : (I : Type) -> (I -> Z) -> Z

(Type is similar to Set1 and above) This can work in Coq if you turn on 
impredicative quantification for Set. The idea of the above type is that I 
acts as an index set, and 'sup I f' represents the set of all sets 'f i' for 
'i : I'. You then encode the power set like:

  Power x = sup (Z -> Prop) ...

However, as I mentioned, this encoding living entirely in Set makes essentialy 
use of impredicativity at this point. You can stratify it using universe 
polymorphism like so:

  data Z {i} : Set (suc i) where
    sup : (I : Set i) -> (I -> Z {i}) -> Z {i}

Although this is a slight pain to use in Agda currently; adding a second level 
parameter might be advisable. Anyhow, then powerset becomes:

  Power : {i : Level} -> Z {i} -> Z {suc i}
  Power {i} x = sup (Z {i} -> Set i) ...

Which works. But we are now using the entire hierarchy of Agda universes while 
ZF would call these all merely 'set'. Powerset is that strong an operation 
(I'm unsure if you could just use (Z {i} -> Set), and have everything happen 
to live in either Set or Set1; perhaps that's an option).

One thing that Agda can do to shrink things down to Set size is define a 
hierarchy of inductive recursive universes. It's possible to define

  U : Nat -> Set
  T : (n : Nat) -> U n -> Set

where each U n is closed under similar operations to Set, and T n interprets 
elements of U n into Set. The definition of Z then could be:

  data Z : Set where
    sup : (n : Nat) (I : U n) -> (T n -> Z) -> Z

This kind of stuff gets a little unwieldy, though, and it isn't essentially 
different from the Z {i} solution above. It's just that induction-recursion 
makes Set 'big enough' to contain an entire hierarchy of universes itself. 
Perhaps it's the solution I've been looking for though (it is, after all, an 
encoding of Z in Agda (without impredicativity) that should both work, and 
live entirely in Set).

Cheers,
-- Dan