Internal Kolmogorov Limits [efr-UOQG]

Let \mathcal {C} \to \mathcal {C}_s be a Markov Promonad with \mathcal {C} itself Cartesian. Suppose \mathcal {C} admits a natural numbers object N. Then we may view a map A \to N \in \mathcal {C} as an indexed family of objects over N. Given such a family, if \mathcal {C} has finite coproducts, we can build a new family A' = A + 1 \to N + 1 \cong N, which corresponds to A'_n = A_{n-1}, A'_0 = 1. Suppose we have a map d: A \to A' over N. This corresponds to a family A_n \to A_{n-1}. Since \Pi _n A'_n = \Pi _n A_n, this induces a map d: \Pi _n A_n \to \Pi _n A_n (here we abuse notation and call this also d). Consider finally the equalizer \Eq (d,1). Its universal property is that a map into it is a map f: N \times X \to A (= \sum _n A_n) over N, with the property that df(n,x) = f(n-1,x) for n > 0.

This is an internal formulation of the universal property of the cofiltered inverse limit \lim (A_0 \leftarrow A_1 \dots ). We will say that \mathcal {C}_s preserves internal sequential inverse limits if it preserves this universal property (observe that this makes sense). As soon as \mathcal {C} has countable coproducts and is (countably) extensive, this is equivalent to an inverse limit in the external sense, where indeed we have many examples of preservation.