There are dualities between the two approaches. We have initial algebras final co-algebras. Least fix points are essentially a set theoretic counterpart initial algebras, and this side we have largest. The concept of congruence gives rise to a certain bisimulation. Induction to co-induction, inductive predicate to invariant predicate. | ![]() |