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