A universal algebra inspired toolkit for working with datatypes in type theory