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!
Comments
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
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!