Pataraia's fixed point theorem gives a constructive proof of the fact that if you have a monotone function $f$ on a DCPO, then it has a least fixed point. I've frequently used this fixed point theorem to construct logical relations for proving properties about dependent type theories.
The idea is that you can view a syntactic type system as a pair $(U, \phi)$ of a partial equivalence relation (or PER) $U$, representing the codes of types, and an interpretation function $\phi : U \to \mathrm{PER}$, sending each type code to its interpretation. Semantic type systems can be equipped with a domain structure, by saying that $(U', \phi') \sqsubseteq (U, \phi)$ just when $U' \subseteq U$, and for every type $A \in |U'|$, we have that $\phi(A) = \phi'(A)$. The empty type system is the obvious bottom element, and joins exist in the obvious way. Then a logical relation can be constructed as a fixed point of a monotone map with respect to this ordering.
However, this semantic definition also bears a strong relationship to inductive-recursive definitions, where the set $U$ and the interpretation $\phi$ are defined simultaneously. (Unsurprisingly, since generalizing universe constructions was the prime motivation for the invention of induction-recursion.)
Has anyone looked at the relation between the two? It's not obvious to me, since the proof of Pataraia's theorem, while constructive, is rather impredicative (it seems to rely essentially upon the powerset operation). So:
- Can Pataraia's theorem be used to prove the soundness of the full induction-recursion schema?
- To what extent can induction-recursion be used to prove the converse? (I assume it won't go all the way, but maybe I'm wrong!)