Isoecursive Types When to Fold and Unfold
As you've stated, the type of IntObject is mu X. {val: int, add: (X -&gt; X)}. fold and unfold witness the isomorphism between a recursive type and its body, i.e. in this case between mu X. {val: int, add: (X -&gt; X)} and {val: int, add: ((mu X. {val: int, add: (X -&gt; X)) -&gt; (mu X. {val: int, add: (X -&gt; X)))}. Letting Y stand for mu X. {val: int, add: (X -&gt; X)}, this can be more compactly written unfold : Y ~= {val: int, add: (Y -&gt; Y)} with fold going the other direction.

You need unfold whenever you want to access any fields/methods. mu X. {val: int, add: (X -&gt; X)} doesn't have any fields; {val: int, add: (Y -&gt; Y)} does. Dually, whenever you want to make an IntObject, you need to use fold. A value of type {val: int, add: (Y -&gt; Y)} is not an IntObject, but fold can inject that value into the type IntObject. In particular, any time you new up an IntObject, i.e. invoke the constructor to create an object.

Basically, your IntObject(i) "really means" something like 

let self = fold({val: i, add: \other -&gt; IntObject.add(self, other)}) in self


Similarly, your add method would look like:

def add(self, other):
    return IntObject(unfold(self).val + unfold(other).val)


where we'd use the definition of IntObject just mentioned above.