Well founded coalgebras Definition 6.2.1 captures the feature which was common to the examples of that section, using parse rather than ev . Proposition 6.3.9 and Theorem 6.3.13 are examples of arguments which use this as an idiom of induction. X is the conclusion. Recall that parse is also mono in a wff-system. Certain ideas from set theory now become useful, where for the purposes of universal algebra in the previous chapter they were a nuisance.
Y t holds.
By Proposition 2.6.2 or Exercise 3.54 . TX X is the initial T -algebra. This is a very convenient diagrammatic form in which to present recursive programs, as we illustrate in Example 6.4.7 and Exercises 6.27 ff. Expand and rearrange the diagram of partial functions. Z Q satisfying the recursion equation.