[Agda] Problem with the termination checker

[David Leduc]

Hi,

In the code below I define a datatype T and then
define a function mylift that will lift
a value of type T l1 into a value of type T (l1 ⊔ l2).

However the termination checker rejects my function mylift :(
How can I convince Agda that mylift terminates?


{-# OPTIONS --universe-polymorphism #-}

module test where

open import Level
open import Coinduction

mutual

 data T (l : Level) : Set (suc l) where
   buildT : (A : Set l) -> (t : ∞ (T l)) -> [ ♭ t ] -> T l

 [_] : {l : Level}(t : T l) -> Set l
 [ buildT A _ _ ] = A

p2 : {l : Level} -> T l -> T l
p2 (buildT _ t _) = ♭ t

p3 : {l : Level}(t : T l) -> [ p2 t ]
p3 (buildT _ _ x) = x

mutual

  mylift : (l1 l2 : Level) -> T l1 -> T (l1 ⊔ l2)
  mylift l1 l2 t = buildT (c1 l1 l2 t) (♯ c2 l1 l2 t) (c3 l1 l2 t)

  c1 : (l1 l2 : Level) -> T l1 -> Set (l1 ⊔ l2)
  c1 l1 l2 t = Lift{l1}{l2} [ t ]

  c2 : (l1 l2 : Level) -> T l1 -> T (l1 ⊔ l2)
  c2 l1 l2 t = mylift l1 l2 t

  c3 : (l1 l2 : Level)(t : T l1) -> [ c2 l1 l2 t ]
  c3 l1 l2 t = p3 (mylift l1 l2 t)