New tools are presented for reasoning about properties of recursively
defined domains. We work within a general, category-theoretic framework
for various notions of `relation' on domains and for actions of domain
constructors on relations. Freyd's analysis of recursive types in terms of
a property of mixed initiality/finality is transferred to a corresponding
property of *invariant* relations. The existence of invariant
relations is proved under completeness assumptions about the notion of
relation. We show how this leads to simpler proofs of the computational
adequacy of denotational semantics for functional programming languages
with user-declared datatypes. We show how the initiality/finality property
of invariant relations can be specialized to yield an induction principle
for admissible subsets of recursively defined domains, generalizing the
principle of structural induction for inductively defined sets. We also
show how the initiality/finality property gives rise to the co-induction
principle studied by the author (Theoretical Computer Science 124(1994)
195-219), by which equalities between elements of recursively defined
domains may be proved via an appropriate notion of `bisimulation'.