[Agda] Type level computation in inductive types

[david.janin at labri.fr]

Dear all, 

Could well be a silly question, but I don’t understand why the following definition does not type in Agda:

data TypedPath {l}  : Set l -> Set l -> Set l where
   atom : ∀ {A B : Set l} -> A -> B -> TypedPath A B
   append : ∀ {A B C : Set l} -> (A -> C) -> TypedPath C B ->  TypedPath A B

Instead, it seems that Agda expects

data TypedPath {l}  : Set l -> Set l -> Set (suc l) where
   ….

with an increase in type universe level. 


As far as I eventually manage to make CoQ prints its (more hidden) universe levels, the inductive type

Inductive hybridPath : Type -> Type -> Type :=
  const: forall A B : Type,  A  -> B -> hybridPath A A
| comp : forall A B C : Type, hybridPath A C 
       -> hybridPath C B -> hybridPath A B.

stays in CoQ within the same level of types….

Any hint welcome,

David