So I was trying to write up this stuff in a constructive context, but ran into a problem that the naive function for arbitrary joins (which has type (set V -> V)) seems to be uncomputable (for V with infinite elements) to me.

Is there a way to restrict this to what we need?