The "function" type $\rightarrow$ is predefined in Agda. But how would one define it if it was not predefined? Specifically I am talking about $\rightarrow$ in:
data Nat : Set where zero : Nat Suc : Nat -> Nat
It is not possible:
-> is built into the underlying logic of Agda (and most dependently typed languages).
-> is not a type constructor, because it has binding properties. Because you can define things like
(n : Nat) -> Vec A n, the compiler needs to add
n to the variables in scope in the right hand side of the arrow, so this can't be done.
There are ways to cheat with bindings. For example, you can define $\exists x : T \ldotp S[x]$ as
ex T (\x -> S), i.e. using a lambda to represent the binding. But, that lambda is typed using
->. Having dependent functions built in is the starter that bootstraps the rest of the type system. It's the only way the language can express quantification, so it ends up being critical.