type-theory Definition Arrow The arrow is a type constructor that maps two types (domain and codomain) to a new type (the function type) :