On 2010-09-24 11:06, David Leduc wrote:
> I now understand the problem but I cannot find a solution. Any
> suggestion?
mutual
↑ : ∀ {ℓ₁} ℓ₂ → T ℓ₁ → T (ℓ₁ ⊔ ℓ₂)
↑ ℓ₂ (buildT A t y) =
buildT (Lift {ℓ = ℓ₂} A) (♯ ↑ ℓ₂ (♭ t)) (↑′ ℓ₂ (♭ t) y)
↑′ : ∀ {ℓ₁} ℓ₂ (t : T ℓ₁) → [ t ] → [ ↑ ℓ₂ t ]
↑′ ℓ₂ (buildT A t y) = lift
--
/NAD