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
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.Sign up to join this community
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.