Sized sequence data-types
A wrapper to make length-parametrized data-type from endofunctors from subcategories.