That's exactly correct.

In a Dependently Typed (DT) language like Agda the language of values and the language of types are one and the same. Thus, a function from types to types is exactly the same sort of thing as a function from values to values. In this case we have a third sort of totally-natural-day-old-kind-of-thing: a function from values of ℕ to types (in Set). It's "just" a function from values to types.

Now, we annotate values with their types. Thus we might have a new top-level definition

    something : zero even
    something = _

where we've used our postfix `even` function to construct a type from the value `zero`. Is this type inhabited? That's a question of proof and programming. Regardless of its inhabitation, though, we can clearly see that the notion of `zero even` simply being a type is sound---that's the nature of function application when the target domain is that of Set!

An Agda program isn't like a C program; a C program is just a bunch of strings that tells the processor where to go and what to do. An Agda program is, instead, a bunch of strings that one-by-one teaches the typechecker what is true about the world.

In the beginning, there was Set, which is the set of all valid types. It's empty (more or less). Then comes along

    data ℕ : Set

This says that the type ℕ, which will be our natural numbers, belongs in Set. Now Set has one valid type, which is ℕ. But ℕ, which is also a type, is empty. And if there's one thing we know about natural numbers, is that there's lots of them.

So we must tell it what its members are. We COULD do it like this:

    zero : ℕ
    one : ℕ
    two : ℕ
    three : ℕ

But how tedious would that be? Instead, we use induction:

    data ℕ : Set where
        zero : ℕ
        succ : ℕ → ℕ

So zero is a member of ℕ, like before. But the successor of any member in ℕ is also in ℕ. So succ zero, and succ succ zero, and succ succ succ zero.

People see the arrow and they think functions. That's not how I think about it. Functions are great, but when I hear function I think C functions, which are tiny little instructions for tiny little machines and don't make any sense in a dependently-typed world. So instead, when I see the arrow, I think of it as a way of telling the type checker this fact: wherever you see the string "succ n", assign it the type ℕ but ONLY IF "n" is also of type ℕ. Think of the arrow as the lambda abstractor, and the space as the lambda applicator. Maybe that helps a little; maybe it hurts a lot.

We plunge forward!

    _+_ : ℕ → ℕ → ℕ
    zero + n = n
    (succ n) + m = succ (n + m)

More substitution rules. Whenever you see zero + n, the typechecker is allowed to replace it with n. Whenever you see (succ n) + m, it's allowed to replace it with succ (n + m). Allowed, but not required: the typechecker should only use these rules if it needs help typechecking a string it doesn't recognize.

We would now like describe even numbers in Agda. Could we just define

    data even : Set?

And thus give Set its second element? No! Because evenness is a proposition! It _depends_ on our other type ℕ, which is where we get our fancy dependently-typed programming from. We really want to say this:

    data even 0 : Set
    data even 2 : Set
    data even 4 : Set

But that would be tedious. So instead we say

    data even : ℕ → Set

If the arrow means substitution, like before, we can think about it like this: wherever we see the string "even n", assign it the type Set (a.k.a. let it be a valid type) but ONLY IF "n" has type ℕ. Is that true for any n? Nope. If it were, we would write

    data even : ℕ → Set where
        even_everything_is_goddamn_even : (n : ℕ) → even n

Instead, we first assume that "even n" is true for no n at all. That's right: a function with an empty domain. We fill in the domain gradually.

    data even : ℕ → Set where
        even_zero : even zero
        even_succ : (n : ℕ) → even n → even (succ (succ n))

First, even zero means that "even zero" is a member of Set. zero is a natural number, so this typechecks. Second, suppose you have n : ℕ. And suppose even n typechecks. Then even (succ (succ n)) also typechecks.

It's simply another form of induction, although slightly trickier because we're trying to fill out a proposition.

Anyway. Hope that helps more than it confuses. I think Learn You An Agda makes it more confusing that it really is by not explaining Set and by using that weird postfix notation. Set is just Haskell's asterisk kind "*" if you know Haskell; otherwise it's pretty hard to grok for a while.

You should also check out Benjamin Pierce's textbook on Coq programming, which expands on a lot of these details. (Coq and Agda and Idris are all pretty much are built on the same ideas.)

http://www.cis.upenn.edu/~bcpierce/sf/current/index.html

In his example, `ZERO` is a value of type `zero even`. `ZERO` is the "proof" that zero is even. Of course its not much of a proof, rather its true by definition. Similarly `STEP ZERO` is of type `suc(suc(zero)) even` and thus a "proof" that two is even.