Working backwards, K is the kernel of a coequaliser, and also gives enough information to allow us to investigate T and W . Exercise 3.60 instead considers the transitive closure as a list of steps, capturing the imperative idiom directly. N from which the results follow by brute force. They may also be proved in a finitary way using the universal properties in a logos. Now we are equipped to justify Remarks 6.4.6 and 6.4.8 and see how the categorical induction and recursion schemes from Section 6.3 restrict to tail recursion.
X be a functional endo-relation in a logos or a pretopos with stable countable unions.
Let E and Q be the equaliser and coequaliser. The construction of W is shown in the diagram below. Treat V W as a subrelation, so the pullbacks are relational composites as shown. The way that W was constructed, as a pullback, makes it the largest well founded subcoalgebra by Exercise 6.17 . W is the unique well founded solution to the fixed point equation in Theorem 6.4.10 .