List-arithmetic distributive categories: Locoi

AbstractA finitely complete category with stable disjoint coproducts and a parameterized list construction is called a locos. The paper proves that the property of being a locos is local in the sense of being inherited by slice categories. This is proven by establishing two important properties of the list construction in this setting.The first of these is that lists can be characterized as objects which satisfy a domain equation and have their tail maps contractions. A contraction is an endomorphism which, when it is applied frequently enough, becomes fixed. It is a central technical notion in this development. As this characterization only uses the number arithmetic of the setting, it provides a powerful tool for establishing the existence of lists.The second result is that list construction preserves and creates connected limits. Because lists satisfy a domain equation they are models of a certain type of sketch. Models of such sketches are preserved and created by connected limits. However, it is the fact that the contractions are also preserved by these limits which is crucial. This observation immediately gives the localness of list construction in a locos and is fundamental to many of the other properties of list construction