[Agda] universum levels

[Andreas Abel]

Levels are there to prevent Hurkens Paradox.  In particular,

   Set : Set

is inconsistent.

On 23.06.2014 11:02, Sergei Meshveliani wrote:
> People,
>
> I am writing a manual on a program written in Agda, and wonder:
> what brief explanation words to set about an  universum level
> (l : Level) ?
>
> I know only that
> (1) each type belongs to some universums,
> (2) each universum has its level  l : Level,
> (3) Level  has the operations  suc, _⊔_,
> (4) Agda can show some level expression for each given type.
>
> Is it true that for each type Agda finds a minimal universum level ?

Well, you give the level yourself.

> Is it true that each level universum is
>                                           U(l) = all types of level <= l
> ?

Yes.

> It is true that
>             All types =  U(0) union U(suc 0) union U(suc $ suc 0) ...
> ?

Yes.

> Approximately and briefly, what notion does Level express?

The "size" of sets (e.g. given by inaccessible cardinals).

> Is it related to the relative algorithmic decidability or
> enumerability?

No.

It is related to Grothendieck Universes or large cardinals.

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/