Thanks, this is a nice approach to construction. I am accepting the other answer only because it is slightly smaller, but I wish I could accept both answers.

If we define $\alpha_i := \mathsf K_1$, it looks like we can simplify this example further by taking $\mathbb D$ to be a 3-element monoid (by removing $\mathsf{swap}$) rather than a 4-element monoid. Does this sound right to you?

Could you provide a list of results for 1- or 2-categorical geometric morphisms that you'd like analogues of for double categories? There's no comprehensive study of such things for double categories, but perhaps if you have results in mind, then we can provide references.

Are there facts in the 1-categorical setting about geometric morphisms you would like to know hold for double categories? I'm not sure what kind of facts you're looking for.

If you mean simply an adjunction in which the left adjoint preserves finite limits, this definition makes sense immediately for double categories: i.e. the left adjoint should preserve finite products, equalisers, and tabulators. Are you looking for something else?

I've fixed the broken link.

Could you explain which part of the proof specifically you are having trouble understanding? I don't see any coend calculus, for instance, and Street gives a precise reference for the monadicity result he uses.