In Robert Paré's 2018 presentation "Double Categories: The best thing since slice categories", the slides non-exhaustively give the following listing of interesting situations where double categories arise:
- External/internal
- Total/partial (restriction categories; e.g. Pfn & Set)
- Deterministic/stochastic
- Classical/quantum
- Linear/smooth
- Classical/intuitionistic
- Lax/oplax (MonCat)
- Strong/weak
- Horizontal/vertical (categories of quintets, categories of commuting squares)
I didn't attend the presentation, so I don't know the examples that were used; what are typical examples for each of these situations? I felt that this was small enough for one single question, particularly since somebody might have Paré's original examples, but won't complain if it needs to be split up.
I already know a family of examples for "total/partial"; every restriction category (nLab) can be rearranged into a double category. Also, for "lax/oplax", I gather that the 2-category MonCat of monoidal categories and lax monoidal functors can be turned into a double category with oplax monoidal functors as the other kind of morphism. The slides give examples of generic horizontal-and-vertical-arrow constructions too.