Re: [Agda] Level ω

[David Leduc]

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)