Changes

each ''p'' : ''U''′ → '''B''' has a unique decomposition into a ''p''′ : '''B'''^''n'' → ('''D'''^''n'' → '''B''') and a set of ''p''″ : '''D'''^''n'' → '''B''' such that:

each ''p'' : ''U''′ → '''B''' has a unique decomposition into a ''p''′ : '''B'''^''n'' → ('''D'''^''n'' → '''B''') and a set of ''p''″ : '''D'''^''n'' → '''B''' such that:

: ''p'' : '''B'''^''n'' &times; '''D'''^''n'' &rarr; '''B''' <u>&asymp;</u> ''p''&prime; : '''B'''^''n'' &rarr; ''p''&Prime; : ('''D'''^''n'' &rarr; '''B''').

: ''p'' : '''B'''^''n'' &times; '''D'''^''n'' &rarr; '''B''' <math>\cong</math> ''p''&prime; : '''B'''^''n'' &rarr; ''p''&Prime; : ('''D'''^''n'' &rarr; '''B''').

For the sake of the visual intuition we may imagine that each cell ''x'' in the diagram of ''U'' has springing from it the diagram of the proposition ''p''&prime;(''x'') = ''p''&Prime; in d''U''.

For the sake of the visual intuition we may imagine that each cell ''x'' in the diagram of ''U'' has springing from it the diagram of the proposition ''p''&prime;(''x'') = ''p''&Prime; in d''U''.

From a theoretical perspective the issue of this difference (between the extended function p and its decomposition p'* p") may seem trifling and, in view of the isomorphism, largely in the eye of the beholder.  But we are treading the ground between formal parameters and actual variables, and experience in computation has taught us that this distinction is not so trivial to treat properly in the "i" of a concrete interpreter.  With this level of concern and area of application in mind the account so far is still insufficiently clear.

From a theoretical perspective the issue of this difference (between the extended function ''p'' and its decomposition ''p''&prime;<math>\cdot</math>''p''&Prime;) may seem trifling and in view of the isomorphism largely in the eye of the beholder.  But we are treading the ground between formal parameters and actual variables, and experience in computation has taught us that this distinction is not so trivial to treat properly in the "''i''" of a concrete interpreter.  With this level of concern and area of application in mind the account so far is still insufficiently clear.

To attempt a clarification let us now make one more pass.  Let x and y be variables ranging over U and dU, respectively.  Then each p: U' = U x dU -> B has a unique decomposition into a p': U -> B and a set of p(x)': dU -> B such that

To attempt a clarification let us now make one more pass.  Let ''x'' and ''y'' be variables ranging over ''U'' and d''U'', respectively.  Then each ''p''&nbsp;:&nbsp;''U''&prime; = ''U''&nbsp;&times;&nbsp;d''U''&nbsp;&rarr;&nbsp;'''B''' has a unique decomposition into a ''p''&prime;&nbsp;:&nbsp;''U''&nbsp;&rarr;&nbsp;'''B''' and a set of ''p''(''x'')&prime;&nbsp;:&nbsp;d''U''&nbsp;&rarr;&nbsp;'''B''' such that

: p(x,y) = p'(x)(y) = p(x)'(y).

: ''p''(''x'', ''y'') = ''p''&prime;(''x'')(''y'') = ''p''(''x'')&prime;(''y'').

The "x" in p(x)'(y) would ordinarily be subscripted as a parameter in the form px', but this does not explain the difference between a parameter and a variable.  Here the difference is marked by the position of the prime ('), which serves as a kind of "run-time marker".  The prime locates the point of inflexion in a piece of notation that is the boundary between local and global responsibilities of interpretation.  It tells the intended division between individual identity of functions (a name and a local habitation) and "socially" defined roles (signs falling to the duty of a global interpreter).  In the phrase p'(x) the p' names the function while the parenthetical (x) is part of the function notation, to be understood by a global interpreter.  In p(x)' the parenthetical (x) figures into the name of an individual function, having a local significance but only when x is specified.

The "x" in p(x)'(y) would ordinarily be subscripted as a parameter in the form px', but this does not explain the difference between a parameter and a variable.  Here the difference is marked by the position of the prime ('), which serves as a kind of "run-time marker".  The prime locates the point of inflexion in a piece of notation that is the boundary between local and global responsibilities of interpretation.  It tells the intended division between individual identity of functions (a name and a local habitation) and "socially" defined roles (signs falling to the duty of a global interpreter).  In the phrase p'(x) the p' names the function while the parenthetical (x) is part of the function notation, to be understood by a global interpreter.  In p(x)' the parenthetical (x) figures into the name of an individual function, having a local significance but only when x is specified.