in locally Cartesian closed categories (LCCCs) and yet more generally in categories with pullbacks.

In our mathematics, we use syntax similar to the dependently typed functional programming language Agda [@norell:thesis; @agda]. If some function argument will be derivable in most contexts, we mark it as implicit by enclosing it/its type in braces in the function’s type declaration and either give this argument in braces or omit it in the definition and applications of the function.

We have formalized the central parts of the theory presented in Agda. The development is available at <http://cs.ioc.ee/~danel/dcont.html>.

Structure of the Article {#structure-of-the-article .unnumbered}
------------------------

In Section \[sec:containers\], we review the basic theory of containers, showing also some examples. We introduce containers and their interpretation into set functors. We show some constructions of containers such as the coproduct of containers. In Section \[sec:dcontainers\], we revisit our examples and introduce directed containers as a specialization of containers and describe their interpretation into comonads. Our main result, that a container is a comonad exactly when it is directed, is the subject of Section \[sec:pullback\]. In Section \[sec:constructions\], we look at some constructions, in particular the cofree directed container and the focussed container (zipper) construction. In addition, we 