<div dir="ltr"><div>Dear list,</div><div><br></div><div>Help me please. I can not understand what difference between these definitions.</div><div><br></div><div>data T1 {ℓ} : Set ℓ where</div><div> c1 : T1</div><div><br></div><div>data T2 : {ℓ : _} → Set ℓ where</div><div> c2 : T2</div><div><br></div><div>Why first one is approved but second one is rejected with error</div><div>"The sort of T2 cannot depend on its indices in the type {ℓ : Agda.Primitive.Level} → Set ℓ when checking the definition of T2"?</div></div>