I see what you mean with the copying. I just thought based on OPs comments there would have been a strong correspondence between lambda calculus numbers (Church encoding) and the operations on them, and actual type-linear functions.