  Nested datatypes have been widely studied in the past 25 years, both
theoretically using category theory, and practically in programming languages
such as Haskell. They consist in recursive polymorphic datatypes where the type
parameter changes throughout the recursion. They have a variety of applications
such as modelling memory or modelling constraints over regular datatypes
without relying on dependent types. In this work, we focus on a specific subset
of nested datatypes which we call Linked Nested DataTypes (LNDT). We show that
some usual datatypes such has List and Maybe, as well as some well-known nested
datatypes such as Nest and even Bush can be built as various instances of LNDT.
We proceed by presenting LibNDT, a library, developed both in Agda and Coq,
which focuses on the set of constructs that can be spread directly from the
parameter on which a LNDT is built, to the LNDT itself. These spreadable
elements are of two kinds, functions, such as folds and map, and properties,
such as the congruence of map or the satisfaction of a given predicate for at
least one, or all, elements of the structure. We make use of the dependent type
system of both Coq and Agda to model the latter. This paper ends with a
discussion about various interesting topics that were raised throughout our
development such as the issue of termination, the comparison of our tools and
the proof effort required to extend LibNDT with additional elements.
