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.
These look interesting for anyone interested in coinduction:
now also at Coinduction - References.
That entry would deserve to have something in its Examples-section.
I have also added
Why does it say at coinduction?
It generalises to corecursion.
I thought corecursion concerns the existence of a morphism to the terminal coalgebra, and coinduction concerns the non-existenced of a proper quotient of the terminal coalgebra. We really need a proper discussion of bisimulation.
Anyway, I pointed to an example of coinduction.
There’s a handy discussion at Piponi’s blog as to why induction and coinduction seem so different. I guess it’s because if they take place in a concrete category. one is using no proper subalgebra of the initial algebra, so no proper subset of a certain kind, while the other is using no proper quotient of the terminal algebra, so no equivalence relation of a certain kind.
1 to 5 of 5