Datatype-generic programming makes it possible to define a construction once and apply it to a large class of datatypes. This is often useful to avoid code duplication in languages that encourage the definition of custom datatypes. In particular, state-of-the-art dependently-typed languages encourage users to define variants of the same datatype with different type-level invariants, highlighting a desperate need for datatype-generic programming. In addition to giving access to familiar programming constructions for free, datatype-programming in the dependently-type setting allows for useful proof-related constructions. However, the current interfaces available for this purpose are needlessly hard to use or are limited in the range of datatypes they handle. In this paper, we describe the steps undertaken so as to make safe datatype-generic programming available in the Agda programming language. Compared to existing work, our library has the benefit of defining a richer set of constructions that can be used in the safe fragment of Agda. Their interface is mostly free of any reference to the underlying encoding, making it almost as natural to work with as handwritten code. Furthermore, we provide building blocks so that users can too define their own datatype-generic constructions.