[Agda] type of identifier

[Sergei Meshveliani]

Please, how to show the type of an identifier in the interactive
editing?
I expected something like  "position cursor, C-c C-t",  
but do not find.

Thanks,

------
Sergei