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 i d (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 ↦ [id,〈id, 〉]. Properties. Like all constructions defined by a universal property, lists over an object are unique up to canonical isomorphism. The object (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 : → which makes the following diagram commute: