How to define function type in AGDA
It is not possible: -&gt; is built into the underlying logic of Agda (and most dependently typed languages).

In particular, -&gt; is not a type constructor, because it has binding properties. Because you can define things like (n : Nat) -&gt; 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 -&gt; S), i.e. using a lambda to represent the binding. But, that lambda is typed using -&gt;. 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.