Changes

Using the isomorphism between function spaces:

Using the isomorphism between function spaces:

: (Bn x Dn -> B) <==> (Bn -> (Dn -> B)),

: ('''B'''^''n''&nbsp;&times;&nbsp;'''D'''^''n''&nbsp;&rarr;&nbsp;'''B''') &asymp; ('''B'''^''n'' &rarr; ('''D'''^''n'' &rarr; '''B''')),

each p: U' -> B has a unique decomposition into a p': Bn -> (Dn -> B) and a set of p": Dn -> B such that:

each ''p'' : ''U''&prime' &rarr; '''B''' has a unique decomposition into a ''p''&prime; : '''B'''^''n'' &rarr; ('''D'''^''n'' &rarr; '''B''') and a set of ''p''&Prime; : '''D'''^''n'' &rarr; '''B''' such that:

: p : Bn x Dn -> B <==> p' : Bn -> p": (Dn -> B).

: ''p'' : '''B'''^''n'' &times; '''D'''^''n'' &rarr; '''B''' &asymp; ''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'(x) = p" in dU.

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'* 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.