Does dependent type checkers need to store lambda parameter type in their core language?
In general, type inference for dependent types is undecidable. This means that when checking a function, we need some way to know what type its argument has.

In the case of Idris, they simply annotate lambdas with parameter types. This is very common in type theory, since it makes your type system syntax directed in a very simple way. When you do this, you can usually view the typing judgment as having the type as an output parameter (i.e. given the input term, you can determine its type).

I don't know what MiniAgda does in particular, but the other main way is to treat the type as an input to the checking judgment. So in this case, you don't need to store the type of the function in the AST, but when typechecking, you will use the context in some way to get the type of the function (i.e. from an annotation).

Generally this is done using bidirectional typechecking. This paper and this post both give excellent overviews of how this can be done in practice.