The short answer is that, no, there does not (yet) exist a good introduction/reference for double category theory. Part of the reason for this is that double category theory only started to enjoy a sustained level of research in the last 25 years, whereas 2- and bicategory theory have been continually studied since the mid 1960s. This means that there are fundamental aspects of double category theory are not yet entirely settled. However, now that double categories are becoming an established aspect of category theory, such a reference would certainly be welcome.
For now, let me give references for some fundamental topics in double category theory that I think give a good foundation for an aspiring double category theorist. This will not be exhaustive, and I will most likely add more in the future.
(First, let me mention that although Grandis's book Higher Dimensional Categories does appear to contain a lot of material, my understanding is that it is essentially a compilation of Grandis's papers with Paré: that is, you can find essentially all of the content of book freely in their joint papers.)
Fundamentals
- Limits in double categories (Grandis and Paré, 1999). The starting point for modern (pseudo) double category theory, in which many of the fundamental notions (double categories and their functors, coherence, limits) are developed.
- Adjoint for double categories (Grandis and Paré, 2004). Introduces companions and conjoints (in this paper called vertical companions and orthogonal adjoints), and studies adjunctions between double categories.
- Framed bicategories and monoidal fibrations (Shulman, 2008). Develops the theory of double categories with companions and conjoints (a.k.a. fibrant double categories or equipments). In addition to containing much new material, this is a very good introductory reference to double category theory.
- Yoneda theory for double categories (Paré, 2011). Studies the Yoneda embedding of double categories and introduces modules and multimodulations for double functors, which reveals subtleties in the theory of double categories, and in particular the value of virtual double categories in the fundamental theory.
Further reading
- The span construction (Dawson, Paré, Pronk 2010). Studies the construction of a (covirtual) double category of spans, and exhibits a universal property.
- A unified framework for generalized multicategories (Cruttwell and Shulman, 2010). Introduces virtual equipments (i.e. the virtual double categorical analogue of double categories with companions and conjoints) and develops their theory. Gives a universal property of the monads-and-bimodules construction as the normal functor coclassifier.
- Span, cospan, and other double categories (Niefield, 2012). Examines the relationship between the span construction and tabulators.
- Algebraic Kan extensions in double categories (Koudenburg, 2015). Studies monads on double categories and their algebras, and Kan extensions in double categories of algebras.
- Discrete Double Fibrations (Lambert, 2021). Extends Paré's double category of elements construction to an equivalent between double presheaves and discrete double fibrations.
- Cartesian double theories (Lambert and Patterson, 2023). Introduces a double category theoretic notion of algebraic theory, which gives a convenient method to build new double categories.
- Products in double categories, revisited (Patterson, 2024). Explores more general notions of (co)limit for double categories.