Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I put the constructive version of coalgebra of the real interval there and straightened up the references.
Thanks, Toby! As you know, there is also a coalgebraic description of a half-open interval : the terminal coalgebra for the functor that takes a linearly ordered set to endowed with the lexicographic order. We have material on this at continued fraction.
Now I want to think about whether that can be thickened up to be constructively valid too.
1 to 3 of 3