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.
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 .
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 ↦ [id<sub>1</sub>,〈id<sub>{{var|A}}</sub>, {{var|f}}〉].[1]
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: