  Most texts on Category Theory are written in a very terse style, in which
people pretend a) that all concepts are visualizable, and b) that the readers
can reconstruct the diagrams that the authors had in mind based on only the
most essential cues. As an outsider I spent years believing that the techniques
for drawing diagrams were part of the oral culture of the field, and that the
insiders could read texts on CT reconstructing the "missing diagrams" in them
line by line and paragraph by paragraph, and drawing for each page of text a
page of diagrams with all the diagrams that the authors had omitted. My belief
was wrong: there are lots of conventions for drawing diagrams scattered through
the literature, but that unified diagrammatic language did not exist. In this
chapter I will show an attempt to reconstruct that (imaginary) language for
missing diagrams: we will see an extensible diagrammatic language, called DL,
that follows the conventions of the diagrams in the literature of CT whenever
possible and that seems to be adequate for drawing "missing diagrams" for
Category Theory. Our examples include the "missing diagrams" for adjunctions,
for the Yoneda Lemma, for Kan extensions, and for geometric morphisms, and how
to formalize them in Agda.
