> There's no ADT in category theory. The only place you might find them is in type theory

I wouldn't say that this is true. Category theory has a definition of product of objects, sum/coproduct of objects, terminal object (unit type), and initial object (empty type). There is a correspondence between type and category theory where a certain type theory is the internal language of a certain category: https://ncatlab.org/nlab/show/computational+trinitarianism

Product: https://ncatlab.org/nlab/show/cartesian+product

Coproduct: https://ncatlab.org/nlab/show/coproduct

Terminal object: https://ncatlab.org/nlab/show/terminal+object

Initial object: https://ncatlab.org/nlab/show/initial+object