Re: [Agda] Level ω

[Andreas Abel]

On Sep 26, 2010, at 7:58 AM, David Leduc wrote:

> It would be so nice if I could use Setω :(
>
> OK, I shall ask for less. Suppose that I make sure that all the levels
> in my stream of level are less than or equal to a given level max.
> Then my stream of Sets is in Set (suc max).  How can I convince Agda
> of this fact, i.e., how can I fill the hole in the code below?
>
>
> {-# OPTIONS --universe-polymorphism #-}
>
> module test where
>
> open import Level
> open import Data.Stream
> open import Relation.Binary
>
> infix 4 _≤_
>
> data _≤_ : Rel Level zero where
>  z≤n : ∀ {n}                 → zero  ≤ n
>  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
>
> record BoundedLevel (max : Level) : Set zero where
>  field Carrier : Level
>        Bounded : Carrier ≤ max
>
> open BoundedLevel public
>
> data T (max : Level) : Stream (BoundedLevel max) -> Set ? where
>  makeT : (ls : Stream (BoundedLevel max)) -> Set (Carrier (head ls))  
> ->
>    T max (tail ls)

Can't you do

data T (max : Level) : Stream (BoundedLevel max) -> Set (suc max) where
   makeT : (ls : Stream (BoundedLevel max)) -> Set max -> T max (tail  
ls)

and then define a smart constructor

   makeT' : (ls : Stream (BoundedLevel max)) -> Set (Carrier (head  
ls)) ->
    T max (tail ls)

that does the necessary liftings?


Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

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