MATH.17:4.4 - Construct an operation on operations and its law

Give the higher-order operation its own input and output types. For a transformation sending a function f to a new function T(f), start with an arbitrary input x of the desired new function. Express its required output using f and the available operations. That expression defines T(f)(x). Then establish that the constructed function belongs to the promised output collection.

Choose the law from the needed use. If T is meant to translate a sequence stage by stage, test:

T(g∘f)=T(g)∘T(f) and T(id)=id.

The types on both sides must agree. When T also changes the objects, specify that object assignment and the corresponding operation collections. An assignment preserving these compositions and identities is a functor.

For instance, we want to apply f:A -> B separately to each entry indexed by a fixed set I. Represent the input by s:I -> A; the set of such inputs is A^I. At index i the input is s(i), so the required output is f(s(i)). Collecting these outputs gives the function i -> f(s(i)) from I to B. We have constructed:

L_I(f):A^I -> B^I, defined by [L_I(f)(s)](i)=f(s(i)).

To derive the composition law, take arbitrary s and i:

[L_I(g∘f)(s)](i)=g(f(s(i)))=[(L_I(g)∘L_I(f))(s)](i).

Equality at every index proves the composition law. The identity law follows by applying the identity at every index. If admissibility requires each entry to remain in P, the earlier membership argument applies entry by entry. A condition relating different entries needs a further preservation argument.

A different higher-order operation can have a different useful law. Differentiation of polynomials preserves sums and scalar multiples and obeys the product and chain rules. Use those laws when deriving a derivative; a composition-preservation requirement would ask it to do a different job. The needed mathematical operation determines which laws to establish.