However, Street's note Powerful functors does appear to contain a complete proof.

The nLab is currently incorrect. Lemma 6.1 only contains a proof of one direction.

@TimCampion: do you have a reference for (5)? (It's easy to prove, but it would be useful to be able to cite something.)

If $P$ and $P'$ are products of $A$ and $B$ there may be multiple isomorphisms between them, for instance if $A$ or $B$ have any nontrivial automorphisms.

Did you try emailing Andre Scedrov? He seems the most likely to have a copy of the notes if they still exist.

My impression is not that allegories were made famous by "Categories, Allegories", but rather that this is the first published account of allegories. I cannot find anything to suggest otherwise in the literature.

Jason Brown has described the free cocompletion of a 2-category under (op)lax colimits of 2-functors in his PhD thesis. I shall add a link when the thesis becomes available.

The category of 2-categories is cartesian closed, and so has a cartesian product. Is this what you're looking for?

Very nice argument!

(There is another distinction, which is that Freyd and Street's characterisation is relevant to the 2-category of large categories, whereas Di Liberti–Loregian's is relevant to the 2-category of locally small categories.)

@TimCampion: it is not clear that Freyd and Street's characterisation holds for any example other than ordinary categories (see this question, for instance). On the other hand, if Di Liberti–Loregian's definition captures smallness, I would expect it to immediately generalise to enriched and internal categories.