  Andrew Pitts' framework of relational properties of domains is a powerful
method for defining predicates or relations on domains, with applications
ranging from reasoning principles for program equivalence to proofs of adequacy
connecting denotational and operational semantics. Its main appeal is handling
recursive definitions that are not obviously well-founded: as long as the
corresponding domain is also defined recursively, and its recursion pattern
lines up appropriately with the definition of the relations, the framework can
guarantee their existence. Pitts' original development used the Knaster-Tarski
fixed-point theorem as a key ingredient. In these notes, I show how his
construction can be seen as an instance of other key fixed-point theorems: the
inverse limit construction, the Banach fixed-point theorem and the Kleene
fixed-point theorem. The connection underscores how Pitts' construction is
intimately tied to the methods for constructing the base recursive domains
themselves, and also to techniques based on guarded recursion, or
step-indexing, that have become popular in the last two decades.
