Equality of Recursive and Set Based Approaches

Finding the least fixed point is useful, but we still cannot be entirely sure that the set based definition of the inductive type is equivalent to the recursive definition.

We know from a prior lecture that is the least closed set, which we consider equivalent to the recursive-induction principle. Therefore, if we can show that this union of sets is equivalent to , then our two approaches must yield the same result.
In section 1.2 we provided the fact that for all ordinals , which includes our least fixed point . We also know that , so

Likewise, we know by definition that is a subset of any -closed set. Clearly, is -closed, therefore

Since we have subset inclusion in both directions, it follows that . Given this, we can conclude that the set based definition of inductive types is consistent with the recursive definition.