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:
  1. an object ,
  2. a morphism : 1 → , and
  3. a morphism : × →
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 and. The notation * is sometimes used to denote lists over.

Equivalent definitions

In a category with a terminal object 1, binary coproducts, and binary products, a list object over can be defined as the initial algebra of the endofunctor that acts on objects by ↦ 1 + and on arrows by ↦ .

Examples

Like all constructions defined by a universal property, lists over an object are unique up to canonical isomorphism.
The object 1 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: