Changes

Second, the singular propositions <math>\mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B},</math> picking out as they do a single cell or a coordinate tuple <math>\mathbf{x}</math> of <math>\mathbb{B}^n,</math> become the carriers or the vehicles of a certain type-ambiguity that vacillates between the dual forms <math>\mathbb{B}^n</math> and <math>(\mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B})</math> and infects the whole hierarchy of types built on them.  In other words, the terms that signify the interpretations <math>\mathbf{x} : \mathbb{B}^n</math> and the singular propositions <math>\mathbf{x} : \mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B}</math> are fully equivalent in information, and this means that every token of the type <math>\mathbb{B}^n</math> can be reinterpreted as an appearance of the subtype <math>\mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B}.</math>  And vice versa, the two types can be exchanged with each other everywhere that they turn up.  In practical terms, this allows the use of singular propositions as a way of denoting points, forming an alternative to coordinate tuples.

Second, the singular propositions <math>\mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B},</math> picking out as they do a single cell or a coordinate tuple <math>\mathbf{x}</math> of <math>\mathbb{B}^n,</math> become the carriers or the vehicles of a certain type-ambiguity that vacillates between the dual forms <math>\mathbb{B}^n</math> and <math>(\mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B})</math> and infects the whole hierarchy of types built on them.  In other words, the terms that signify the interpretations <math>\mathbf{x} : \mathbb{B}^n</math> and the singular propositions <math>\mathbf{x} : \mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B}</math> are fully equivalent in information, and this means that every token of the type <math>\mathbb{B}^n</math> can be reinterpreted as an appearance of the subtype <math>\mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B}.</math>  And vice versa, the two types can be exchanged with each other everywhere that they turn up.  In practical terms, this allows the use of singular propositions as a way of denoting points, forming an alternative to coordinate tuples.

For example, relative to the universe of discourse [''a''₁,&nbsp;''a''₂,&nbsp;''a''₃] the singular proposition ''a''₁&nbsp;''a''₂&nbsp;''a''₃&nbsp;:&nbsp;'''B'''³&nbsp;<font face=symbol>'''××>'''</font>&nbsp;'''B''' could be explicitly retyped as ''a''₁&nbsp;''a''₂&nbsp;''a''₃&nbsp;:&nbsp;'''B'''³ to indicate the point <font face=system>‹1,&nbsp;1,&nbsp;1›</font>, but in most cases the proper interpretation could be gathered from context.  Both notations remain dependent on a particular basis, but the code that is generated under the singular option has the advantage in its self-commenting features, in other words, it constantly reminds us of its basis in the process of denoting points.  When the time comes to put a multiplicity of different bases into play, and to search for objects and properties that remain invariant under the transformations between them, this infinitesimal potential advantage may well evolve into an overwhelming practical necessity.

For example, relative to the universe of discourse <math>[a_1, a_2, a_3]\!</math> the singular proposition <math>a_1 a_2 a_3 : \mathbb{B}^3 \xrightarrow{s} \mathbb{B}</math> could be explicitly retyped as <math>a_1 a_2 a_3 : \mathbb{B}^3</math> to indicate the point '''&lsaquo;1,&nbsp;1,&nbsp;1&rsaquo;''', but in most cases the proper interpretation could be gathered from context.  Both notations remain dependent on a particular basis, but the code that is generated under the singular option has the advantage in its self-commenting features, in other words, it constantly reminds us of its basis in the process of denoting points.  When the time comes to put a multiplicity of different bases into play, and to search for objects and properties that remain invariant under the transformations between them, this infinitesimal potential advantage may well evolve into an overwhelming practical necessity.

===The Analogy Between Real and Boolean Types===

===The Analogy Between Real and Boolean Types===