1. Formal definition
     Equivalent definitions  

2. Examples

3. Properties

4. References

5. See also

In category theory, an abstract mathematical discipline, 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 {{var|C}} be a category with finite products and a terminal object 1.

A list object over an object {{var|A}} of {{var|C}} is:

1. an object {{var|L}}_{{var|A}},
2. a morphism {{var|o}}_{{var|A}} : 1 → {{var|L}}_{{var|A}}, and
3. a morphism {{var|s}}_{{var|A}} : {{var|A}} × {{var|L}}_{{var|A}} → {{var|L}}_{{var|A}}

such that for any object {{var|B}} of {{var|C}} with maps {{var|b}} : 1 → {{var|B}} and {{var|t}} : {{var|A}} × {{var|B}} → {{var|B}}, there exists a unique {{var|f}} : {{var|L}}_{{var|A}} → {{var|B}} such that the following diagram commutes:

where 〈id_{{var|A}}, {{var|f}}〉 denotes the arrow induced by the universal property of the product when applied to id_{{var|A}} (the identity on {{var|A}}) and {{var|f}}. The notation {{var|A}}* (à la Kleene star) is sometimes used to denote lists over {{var|A}}. {{sfn|Johnstone|2002|loc=A2.5.15}}

Equivalent definitions

In a category with a terminal object 1, binary coproducts (denoted by +), and binary products (denoted by ×), a list object over {{var|A}} can be defined as the initial algebra of the endofunctor that acts on objects by {{var|X}} ↦ 1 + ({{var|A}} × {{var|X}}) and on arrows by {{var|f}} ↦ [id₁,〈id_{{var|A}}, {{var|f}}〉].^[1]

Examples

• In Set, the category of sets, list objects over a set {{var|A}} are simply finite lists with elements drawn from {{var|A}}. In this case, {{var|o}}_{{var|A}} picks out the empty list and {{var|s}}_{{var|A}} corresponds to appending an element to the head of the list.
• In the calculus of inductive constructions or similar type theories with inductive types (or heuristically, even strongly typed functional languages such as Haskell), lists are types defined by two constructors, nil and cons, which correspond to {{var|o}}_{{var|A}} and {{var|s}}_{{var|A}}, respectively. The recursion principle for lists guarantees they have the expected univeral property.

Properties

Like all constructions defined by a universal mapping property, lists over an object are unique up to canonical isomorphism.

The object {{var|L}}₁ (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 {{var|L}}_{{var|A}} to be the unique morphism {{var|l}} : {{var|L}}_{{var|A}} → {{var|L}}₁ which makes the following diagram commute:{{sfn|Johnstone|2002|p=117}}

References

• {{Cite book|url=https://www.worldcat.org/oclc/50164783|title=Sketches of an Elephant: a Topos Theory Compendium|last=Johnstone|first=Peter T.|date=2002|publisher=Oxford University Press|isbn=0198534256|location=Oxford|oclc=50164783}}

See also

• Natural number object
• F-algebra
• Initial algebra

• List of ships built at Framnaes shipyard
• List of ships built by John Brown & Company
• List of ships captured by pirates off the coast of Somalia
• List of ships captured by Somali pirates
• List of ships captured or attacked by Somali pirates
• List of ships held by Somali pirates
• List of ships in Battlestar Galactica
• List of ships in British Columbia
• List of ships named after Indiana
• List of ships named Fulton
• List of ships named HMY Victoria and Albert
• List of ships named Kaiser Wilhelm II
• List of ships named Kungsholm
• List of ships named Matsonia
• List of ships named Noordam
• List of ships named Sovereign
• List of ships named SS Ohio
• List of ships named SS Rotterdam
• List of ships named SS St. Louis
• List of ships named SS Vaterland
• List of ships of Algeria
• List of ships of the Brazilian Navy
• List of ships of the Canadian Navy
• List of ships of the Chilean Navy
• List of ships of the Danish Navy