In A1, if we view the number as the function type , and as the application , we can reinterpret the numbers , , , and as functions of type , , , and . The definition in A1 then translates to , that is, is defined to be composition of and understood as functions. So the content of A1 amounts to defining term application to be essentially composition, modulo the need to transpose the -tuple to make the types match up suitably for composition. This composition is the one in Lawvere's previously mentioned category of power sets and their functions. In this way we have translated the commuting diagrams of that category, as the equational theory of Boolean algebras, into the equational consequences of A1 as the logical representation of that particular composition law.
