where and might coincide. There is a monoidal product on given by cospan composition (formed by taking pushouts); this monoidal product is denoted . (Explicitly, is .) The monoidal unit is a -element set with its unique bipointed structure. The category of such cospans or bipointed sets is denoted .
Inside is the full subcategory of two-pointed sets, where and are distinct. Let be the category of two-pointed sets. The monoidal product restricts to a functor
and one can define the square
A -coalgebra is a two-pointed set together with a map . An example is given by , where is identified with the interval and the coalgebra structure is identified with multiplication by , . This map will be denoted .
is terminal in the category of -coalgebras.
We now define a number of operations on . For , define and . These give unary operations on which can also be defined as maps in using the coalgebra structure :
We similarly define unary operations , for any -coalgebra . For any coalgebra and , either or . Moreover, if and are the evident pushout inclusions, we have if , and if . This means that coalgebra structures can be recovered from algebraic structures consisting of two constants and two unary operations , , although we must consider a coherent but non-algebraic axiom
Next, we define meet and join operations on , making it a lattice, by exploiting corecursion. A slick corecursive definition of the order is that
if and , or
if and .
If one prefers to work with operations, one could define the meet operation by putting a suitable coalgebra structure on and using terminality of the coalgebra to define as a coalgebra map. A coalgebra structure
which works is
if or ;
The general midpoint operation is not as easy to construct as one might think, but to start with we do have operations which take the midpoint between a given point and an endpoint. Namely, the left midpoint operation is the unary operation defined by
and the right midpoint operation is defined by
There are two versions of this construction, classically equivalent, in constructive mathematics, one of which produces the unit interval of MacNeille real numbers, the other of which produces the unit interval of located Dedekind real numbers. Both start with (which is straightforward) but define differently, and the monoidal product is subtler.
For the MacNeille real numbers, define in the most obvious way,
For the Dedekind real numbers, define by requiring
In , let be a subset of , with iff
(A pushout can be constructed using instead; this is stronger in intuitionistic logic but equivalent assuming excluded middle. If equality happens to be stable in and , then only the classical de Morgan law is needed to make this a pushout.)
As in the classical case, this makes and into semigroupal categories, since the unit object (which exists in as the singleton) does not exist in or in , but we can still define and and consider their coalgebras. As stated above, is the final coalgebra of , and is the final coalgebra of ; both are equipped with and .
Another approach to the Dedekind real interval looks simpler from the perspective of constructive analysis. Start with , the category of point–point apartness spaces and strongly extensional functions between them. (A point–point apartness space is a set equipped with an apartness relation, that is a binary relation satisfying properties dual to those of an equivalence relation; it is iff the apartness relation is tight; and a function between such spaces is strongly extensional iff it reflects .) On , let be the subset of satisfying
Now defining on , its final coalgebra is again the Dedekind unit interval (equipped with its endpoints).
… explain how the classical version corresponds to computation with (unsigned) binary digits … the constructive (Dedekind) version corresponds to computation with signed binary digits …
The original development by Freyd is
The constructive version is also due to Freyd:
Freyd published 8 years later:
There is also a complete development in the Elephant: