I have strong evidence the manuscript exists, since Marta Bunge describes it in an email (check my latest edit). I am currently waiting from a response from her regarding the manuscript.

Michael Barr said he was unaware of the manuscript's existence. I shall continue asking academics who seem like they may know.

Thanks, I shall do so next. I asked Robert Paré and he said that he no longer has a copy; I agree Barr seems a likely candidate.

My understanding is that the manuscript contains a precise statement and proof of the monadicity theorem. I asked Robert Paré and he confirmed that he had at one time a copy of the manuscript, but no longer knows where it is. I plan to reach out to more people soon.

More generally, a formal duality principle could be stated for any 2-category with a duality involution. However, the induction is so trivial I'd be surprised if anyone has written it out explicitly. The one place I could imagine it having been done is in a formalisation of category theory, such as in a category theory library for a proof assistant (e.g. UniMath, or HoTT-Agda); perhaps it'd be worth taking a look at some of these.

@MikeShulman: I see, thanks!

Is there a way to avoid making these size assumptions? It seems reasonable to want to talk about small-cocomplete categories without fixing some inaccessible cardinal.

Thanks! I had completely overlooked that closed classes must include the absolute colimits.

@SergeiBurkin: the presentation of an abstract clone in terms of operations and equations can be translated into an operadic definition in terms of trees and substitution. The set of colours is given by $\mathbb N$, and each of the operations of the theory of clones defines a tree. Is this the sort of description you are looking for? I could spell out the definition if it's not clear.