[Agda] Universe polymorphism

[Nils Anders Danielsson]

On 2009-09-25 17:17, Ulf Norell wrote:
>   At present there is no way to lift types from one level to another, that
>   is, there is no function
> 
>     lift : {i : Level} -> Set i -> Set (suc i)
> 
>   This is likely to change at some point.

How should, say, Σ-types be defined? There are two obvious alternatives:

  data Σ {i} (A : Set i) (B : A → Set i) : Set i where
    _,_ : (x : A) (y : B x) → Σ A B

  data Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
    _,_ : (x : A) (y : B x) → Σ A B

It may be easier to infer levels if the first definition is used, at
least if lifting is an explicit operation. However, if lifting is
explicit, then the second definition has the advantage that lifting is
not necessary. Will lifting be implicit or explicit?

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.