2.8: definition of dependent function type

The problematic sentence reads: "In that case, the type (a : α) → β a denotes the type of functions f with the property that, for each a : α, f a is an element of β a".   I think that what is actually meant is "the type (a : α) → β denotes...".
