List object

In category theory, an abstract branch of mathematics, and in its applications to logic and theoretical computer science, a list object is an abstract definition of a list, that is, a finite ordered sequence.
Formal definition.
Let C be a category with finite products and a terminal object 1. 
A list object over an object of C is:
such that for any object of with maps : 1 → and : × → , there exists a unique : → such that the following diagram commutes:
where〈id, 〉denotes the arrow induced by the universal property of the product when applied to id (the identity on ) and . The notation * (à la Kleene star) is sometimes used to denote lists over .
Equivalent definitions.
In a category with a terminal object 1, binary coproducts (denoted by +), and binary products (denoted by ×), a list object over can be defined as the initial algebra of the endofunctor that acts on objects by ↦ 1 + ( × ) and on arrows by ↦ [id1,〈id, 〉].
Properties.
Like all constructions defined by a universal property, lists over an object are unique up to canonical isomorphism.
The object 1 (lists over the terminal object) has the universal property of a natural number object. In any category with lists, one can define the length of a list to be the unique morphism : → 1 which makes the following diagram commute: