What's the definition of join on iso-recursive types? In languages with subtyping, there is often a "join" operation defined to compute the least upper bound of two types. It's used in type-checking, for example to find the smallest type that covers both the "then" and "else" branches of an if-statement.

What should the definition of join be for iso-recursive types such as $\mu X.\tau$? I started to write it myself, but realized it gets a little tricky if the recursion in each type is unrolled to a different depth.

If there's a standard reference for this, even better. Benjamin Pierce's "Types and Programming Languages" lists the necessary subtype rules near the end of chapter 21, but doesn't define the join rules.
I thought a bit about this and I am afraid that it is harder than it
looks -- as you suspected! In the spirit of encouraging discussion,
I'll write my chain of thoughts.

The subtyping rules are often defined as judgments of the form t1 &lt;:
t2, where --- is an inductive rule (you can only use them finitely
many times along each path in the derivation tree) and === is
a coinductive rule (you can use it infinitely many times).

t1 &lt;: t2
t'1 &lt;: t'2
=================
t1*t'1  &lt;: t2*t'2

t1 :&gt; t2
t'1 &lt;: t'2
======================
t1 -&gt; t'1 &lt;: t2 -&gt; t'2

========
t &lt;: top

========
bot &lt;: t

------
t &lt;: t

t1 &lt;: t2
t2 &lt;: t3
--------
t1 &lt;: t3

t1[a \ mu a. t1] &lt;: t2
----------------------
(mu a. t1) &lt;: t2

t1 &lt;; t2[a \ mu a. t2]
----------------------
t1 &lt;: (mu a. t2)


I would think you can define the /\ and \/ by turning this into
a three-place judgment. Only showing one half:

t1 /\ t2 = t3
t'1 /\ t'2 = t'3
=========================
t1*t'1 /\ t2*t'2 = t3*t'3

t1 \/ t2 = t3
t'1 /\ t'2 = t'3
==================================
t1 -&gt; t'1 /\ t2 -&gt; t'2 = t3 -&gt; t'3

===============
t1 /\ top &lt;: t1

================
top /\ t2 &lt;: tt2

================
t1 /\ bot &lt;: bot

================
bot /\ t1 &lt;: bot

----------
t /\ t = t

t1 /\ t2 = t12
t12 /\ t3 = t23
-----------------------
(t1 /\ t2) /\ t3 = t123

t1 /\ t23 = t123
t2 /\ t3 = t23
-----------------------
t1 /\ (t2 /\ t3) = t123


(The two halves, /\ and \/, can be factorized with a parametrized
presentation where /\^{-1} is \/ and top^{-1} is bot.)

The problem here are the mu-unfolding rules:

t1[a \ mu a. t1] /\ t2 = t3
---------------------------
(mu a. t1) /\ t2 = t3

t1 /\ t2[a \ mu a. t2] = t3
---------------------------
t1 /\ (mu a. t2) = t3


Clearly there should be a rule that allows to build a (mu a. t3) on
the right-hand side; I think the rules above are probably not
complete.

Some presentations of recursive subtyping have rules of the form:

Gamma, a &lt;: b |- t1 &lt;: t2
---------------------------------
Gamma |- (mu a. t1) &lt;: (mu b. t2)

-------------------------------
Gamma ∋ (t1 &lt;: t2) |- t1 &lt;: t2


(Technically these interact with the induction/coinduction
presentation: you may not use an hypothesis in Gamma without using one
of the coinductive/productive rules first.)

I guess that those could be adapted to:

Gamma, a /\ b = c |- t1 /\ t2 = t3
-----------------------------------------------
Gamma |- (mu a. t1) /\ (mu b. t2) = (mu c . t3)

----------------------------------------
Gamma ∋ (t1 /\ t2 = t3) |- t1 &lt;: t2 = t3


I thought that the syntax/coinduction-based presentations of recursive
subtyping ("Coinductive axiomatization of recursive type equality and
subtyping", Brandt and Henglein, 1997; "Subtyping, Declaratively", Danielsson, 2010) would avoid having to think about the tree-form of mu-types,
but it looks like the syntax alone does not scale that nicely to
defining the meet/join, so maybe going back to the tree presentation
would better reveal what should happen.