Nick Bezhanishvili
email: n.bezhanishvili@uva.nl

Sebastian Enqvist
email: sebastian.enqvist@philosophy.su.se

Jim De Groot

Duality for Instantial Neighbourhood Logic via Coalgebra

Keywords: Duality, Modal logic, Instantial Neighbourhood Logic, Descriptive frames, Coalgebra

Instantial Neighbourhood Logic (INL) has been introduced recently as a language for neighbourhood frames where existential information can be given about what kind of worlds occur in a neighbourhood of a current world. Apart from its semantics, its proof theory and bisimulation games have also been studied. However, conspicuously absent from the treatment of INL is the notion of descriptive frames. This is the gap that we are closing in this paper. We introduce descriptive frames for INL and we prove that these are dual to boolean algebras with instantial operators (BAIOs), which give the algebraic semantics of INL. Our methods for establishing this duality make essential use of coalgebra: we observe that BAIOs are algebras for a functor on the category of boolean algebras and show that this functor is dual to the double Vietoris functor (i.e. the composition of the Vietoris functor with itself), thus obtaining a dual equivalence between double Vietoris coalgebras and BAIOs. The proof of our main result is then completed by showing that double Vietoris coalgebras correspond precisely to descriptive frames. As a corollary we obtain that every extension of INL is sound and complete with respect to descriptive frames, that descriptive frames enjoy the Hennessy-Milner property, and as a result, that finite neighbourhood frames enjoy the Hennessy-Milner property.

Introduction

The concept of duality arises in many areas of mathematics, logic and computer science. The first duality milestone in algebraic logic was the Stone representation theorem [START_REF] Stone | The theory of representations for boolean algebras[END_REF], which described the categorical duality between boolean algebras and so-called Stone spaces. Subsequently, many representation and duality theorems have been established, including a representation theorem for Riesz spaces [START_REF] Yosida | On the representation of vector lattices[END_REF], Priestley duality for distributive lattices [START_REF] Priestley | Representation of distributive lattices by means of ordered Stone spaces[END_REF], and Esakia duality for (bi-)Heyting algebras [START_REF] Esakia | Topological Kripke models[END_REF][START_REF] Esakia | The problem of dualism in the intuitionistic logic and Browerian lattices[END_REF][START_REF] Esakia | Heyting Algebras[END_REF][START_REF] Celani | Easkia duality and its extensions[END_REF].

The first representation theorem in the realm of modal logic was given by Jónsson and Tarski [START_REF] Jónsson | Boolean algebras with operators, Part I[END_REF]. Although op. cit. does not mention modal logic explicitly, it introduces relational semantics and uses the representation theorem to relate algebraic and relational semantics. The full duality between boolean algebras with operators and descriptive general frames was established by Goldblatt [START_REF] Goldblatt | Metamathematics of modal logic I[END_REF], and many other dualities ensued [START_REF] Johnstone | Stone Spaces. Cambridge Studies in Advanced Mathematics[END_REF][START_REF] Celani | Priestley duality, a Sahlqvist theorem and a Goldblatt-Thomason theorem for positive modal logic[END_REF][START_REF] Furber | Unrestricted stone duality for Markov processes[END_REF][START_REF] Mio | Riesz modal logic for markov processes[END_REF].

These dualities are useful because they provide two, algebraic and geometric, perspectives on the same object and allow one to translate results from the algebraic language to the geometric one via (descriptive) frames, and vice versa. For example, this was a key ingredient in Sambin and Vaccaro's simplified proof of the celebrated Sahlqvist completeness theorem in modal logic [START_REF] Sambin | A new proof of Sahlqvist's theorem on modal definability and completeness[END_REF].

A novel system of modal logic for reasoning about neighbourhood frames, called Instantial Neighbourhood Logic (INL), was recently introduced in [START_REF] Van Benthem | Instantial neighbourhood logic[END_REF]. The modalities in INL give existential information about what kind of worlds occur in a neighbourhood of a current world. Motivations for investigating this logic range from topology to games, and from modelling notions of evidence to belief revision. Surprisingly however, a duality result is still absent from the theory of INL, despite an abundance of recent interest in the logic [START_REF] Tuyt | Canonical rules on neighbourhood frames[END_REF][START_REF] Yu | A tableau system for instantial neighborhood logic[END_REF][START_REF] Van Benthem | A propositional dynamic logic for instantial neighbourhood semantics[END_REF][START_REF] Van Benthem | A new game equivalence, its logic and algebra[END_REF][START_REF] Yu | Lyndon interpolation theorem of instantial neighborhood logic -constructively via a sequent calculus[END_REF]. This is the gap we are filling in this paper. We introduce a suitable notion of descriptive frames for INL and prove a (categorical) duality between descriptive INL-frames and boolean algebras with instantial operators (BAIOs). The latter give the algebraic semantics for INL and play the same rôle for INL that boolean algebras with operators play for normal modal logic [START_REF] Blackburn | Modal Logic. Cambridge Tracts in Theoretical Computer Science[END_REF][START_REF] Chagrov | Modal Logic[END_REF] and boolean algebras with monotone operators for monotone modal logic [START_REF] Hansen | Monotonic modal logics[END_REF][START_REF] Hansen | A coalgebraic perspective on monotone modal logic[END_REF].

Our main technical tool for establishing this duality is coalgebra. Coalgebras arise as the dual notion of algebras for a functor and have found many applications in logic and computer science. For example, they are a natural setting for dealing with non-wellfounded data structures such as streams or infinite trees, and, triggered by Moss' paper on coalgebraic logic [START_REF] Moss | Coalgebraic logic[END_REF], they have become a widely-used framework for describing semantics for modal logics [START_REF] Rutten | Universal coalgebra: a theory of systems[END_REF][START_REF] Kupke | Coalgebraic semantics of modal logics: An overview[END_REF][START_REF] Kupke | Algebraic semantics for coalgebraic logics[END_REF][START_REF] Kapulkin | Expressiveness of positive coalgebraic logic[END_REF].

A key feature of the coalgebraic perspective on duality is that, in a sense, it isolates the essential part of the duality. In the case of modal logic, the traditional approach of Jónsson-Tarski duality considers modal algebras as boolean algebras with operators, and directly constructs the dual Kripke frames. From the point of view of coalgebra, this turns out to really be a duality between functors. Once we identify modal algebras as the algebras for a certain functor on the category of boolean algebras and recognise its dual functor as the Vietoris functor, the duality between algebras and coalgebras for these two functors, which piggybacks Stone duality, is a trivial consequence. The same approach works well for other variations of modal logic such as monotone modal logic [START_REF] Hansen | A coalgebraic perspective on monotone modal logic[END_REF] or positive modal logic (which piggy-backs on Priestley duality) [START_REF] Palmigiano | A coalgebraic view on positive modal logic[END_REF]. While these examples have been re-cast in this style with hindsight, we believe that this coalgebraic approach serves as a useful blueprint for establishing dualities for new logics. If a logical system and its algebras are given, and a natural candidate for dual "descriptive frames" is suggested, then proceed as follows:

1. Describe the algebras of the logic as algebras for a functor. 2. Find the dual functor T. 3. Show that T-coalgebras are equivalent to descriptive frames.

In the current paper we use this strategy to prove a duality theorem for INL. First, we observe that BAIOs are algebras for a functor on the category of boolean algebras and homomorphisms. Second, we recall that it was observed in [START_REF] Van Benthem | Instantial neighbourhood logic[END_REF] that the neighborhood semantics of INL corresponds to coalgebras for the double covariant powerset functor. Since Kripke frames are coalgebras for the covariant powerset functor, and modal algebras are dual to Vietoris coalgebras, this suggests that BAIOs should be dual to coalgebras for the double Vietoris functor. We verify that this is indeed the case. Lastly, we show that our descriptive frames are precisely the "double Vietoris coalgebras", in the sense that the categories are isomorphic. Hence, these descriptive frames are dual to BAIOs.

A rather trivial step in this proof is the representation of BAIOs as algebras for a functor I; the functor is simply read off from the defining equations of BAIOs. It was observed by Lutz Schröder (private communication) that the logic INL can be translated into the composition of standard modal logic with itself, and vice versa, in a semantics-preserving manner. This suggests that we could optionally have represented BAIOs as algebras for the functor M•M, where M is the functor whose algebras correspond to modal algebras. Since M is dual to the Vietoris functor, the dual equivalence of M • M-algebras with double Vietoris coalgebras would follow directly (in fact, as a special case of a more general result in [START_REF] Kupke | Stone coalgebras[END_REF]). While this alternative approach has a certain elegance to it, we have opted for a more direct representation of INL-algebras here. The main benefit is that our proof gives a quite standard canonical model construction for INL and its extensions, without a detour via a translation. This makes the duality better suited for dealing with issues like canonicity and Sahlqvist completeness, which we hope to address in future work. We obtain the equivalence of INL-algebras with algebras for M • M as a corollary. Our proof also gives a representation of the double Vietoris functor where the topology is described in terms of the INL-modalities, rather than two layers of box and diamond modalities.

As a corollary of our main duality theorem we obtain that every extension of INL is sound and complete with respect to descriptive frames, that descriptive frames enjoy the Hennessy-Milner property, and as a result, that finite INLframes enjoy the Hennessy-Milner property.

Outline. The paper is structured as follows: In Section 2 we recall the definitions of Instantial Neighbourhood Logic and its semantics, algebras and coalgebras, Stone duality, and the Vietoris functor. In Section 3 we define boolean algebras with instantial operators and descriptive INL-frames. The main results of the paper appear in Section 4, where we prove that the category of BAIOs is dually equivalent to the category of coalgebras for the double Vietoris functor, and in Section 5, where we identify coalgebras for the double Vietoris functor with descriptive INL-frames. Finally, we provide some applications of the developed theory in Section 6, and discuss possible direction for future work in Section 7.

Acknowledgements. The authors would like to thank the reviewers of CMCS 2020 for their helpful comments, which improved the presentation of the paper.

Preliminaries

Instantial neighbourhood logic

We briefly recall the language and semantics of instantial neighbourhood logic from [START_REF] Van Benthem | Instantial neighbourhood logic[END_REF]. The language L(Prop) of instantial neighbourhood logic over some arbitrary but fixed set Prop of proposition letters is defined recursively by

ϕ ::= | p | ¬ϕ | ϕ ∧ ϕ | (ϕ 1 , . . . , ϕ n ; ϕ),
where p ∈ Prop and n ∈ ω. Observe that we have a countably infinite number of modal operators: one for each n ∈ ω. Formulas in L(Prop) can be interpreted in neighbourhood frames, which we shall call INL-frames. Definition 2.1. An INL-frame is a pair (X, N ) comprised of a set X and a neighbourhood functor N : X → PPX, where P is the (covariant) powerset functor. A neighbourhood model is a tuple (X, N, V ) where (X, N ) is a neighbourhood frame and V : Prop → PX is a valuation of the proposition letters.

An INL-morphism from (X, N ) to (X , N ) is a map f : X → X such that

N (f (x)) = {f [a] | a ∈ N (x)},
for all x ∈ X. Here f [a] denotes the direct image of a under f . An INL-morphisms (X, N, V ) → (X , N , V ) between neighbourhood models is an INL-morphism f between the underlying frames which additionally satisfies

x ∈ V (p) iff f (x) ∈ V (p)
for every p ∈ Prop. Write INL and INL M for the categories of neighbourhood frames and neighbourhood models, respectively, with their corresponding notion of morphism.

The interpretation of INL formulas in a neighbourhood model (X, N, V ) is defined recursively, where the classical connectives are treated in the standard manner. For the modalities, let x (ϕ 1 , . . . , ϕ n ; ψ) if there is a neighbourhood w ∈ N (x) of x such that y ψ for all y ∈ w, and for each ϕ i there is y i ∈ w such that y i ϕ i . We write ϕ = {x ∈ X | x ϕ} and say that x satisfies ϕ if x ∈ ϕ . Two states are called logically equivalent if they satisfy precisely the same formulas.

The interpretation of the modalities can be conveniently reformulated using the following notion of witnesses. Definition 2.2. Let X be a set and w, a 1 , . . . , a n , b subsets of X. We say that w witnesses (a 1 , . . . , a n ; b) if and only if w ∩ a i = ∅ for all i ∈ {1, . . . , n} and w ⊆ b. We say that w co-witnesses (a 1 , . . . , a n ; b) if and only if w ⊆ a i for some i ∈ {1, . . . , n} or w ∩ b = ∅.

It is straightforward to see that in a neighbourhood model (X, N, V ) a state x satisfies (ϕ 1 , . . . , ϕ n ; ψ) if there is a w ∈ N (x) witnessing ( ϕ 1 , . . . , ϕ n ; ψ ). When there is no danger of confusion, we suppress the subscript n from m ,n .

Yet another way to view the interpretation of the modalities in a neighbourhood model is via the equality (ϕ 1 , . . . , ϕ n ; ψ) = m ( ϕ 1 , . . . , ϕ n , ψ ).

Stone Duality

Write BA for the category of boolean algebras and homomorphisms, and Stone for the category of Stone spaces and continuous functions.

The contravariant functor uf : BA → Stone takes a boolean algebra B to the collection ufB of ultrafilters of B topologized by the base

B = { b | b ∈ B}, where b = {u ∈ ufB | b ∈ u}. The action of uf on a homomorphism h : B → B in BA is defined by (ufh)(u ) = h -1 (u ).
In the converse direction, the contravariant functor clp : Stone → BA takes a Stone space to its boolean algebra of clopens and a continuous function to its inverse. The functors uf and clp constitute a dual equivalence between BA and Stone.

Algebra, Coalgebra, and the Vietoris functor

We recall the definitions of algebras, coalgebras, and the Vietoris functor. Definition 2.4. Let F be an endofunctor on a category C. An F-coalgebra is a pair (c, γ) such that γ :

c → Fc is a morphism in C. An F-coalgebra morphism (c, γ) → (c , γ ) is a morphism f : c → c in C satisfying γ • f = Ff • γ.
The collection of F-coalgebras and F-coalgebra morphisms constitutes the category Coalg(F).

The dual notion of a coalgebra is that of an algebra: an F-algebra is a morphism γ :

Fc → c in C, an F-algebra morphism (c, γ) → (c , γ ) is a morphism f : c → c in C such that γ • Ff = f • γ,

and they form the category Alg(F).

Coalgebras for an endofunctor on Set are used to describe systems [START_REF] Rutten | Universal coalgebra: a theory of systems[END_REF], but can also be used to characterise the frame semantics for a wide variety of modal logics [START_REF] Kupke | Coalgebraic semantics of modal logics: An overview[END_REF]. In particular, as noted in [3, Section 7.5], we have:

Proposition 2.

The category INL of INL-frames and INL-morphisms is isomorphic to Coalg(PP).

In the realm of modal logic a well-known example of a category of algebras is the category MA of modal algebras: we have MA ∼ = Alg(M), where M is an endofunctor on the category BA of boolean algebras and homomorphisms defined as follows: Definition 2.6. For a boolean algebra B let MB be the free boolean algebra generated by the set { a | a ∈ B}, modulo the relations a ∧ b = (a ∧ b) and = . This assignment extends to an endofunctor on BA by defining the action of M on a homomorphism h : B → B via Mh( a) = h(a) and extending this (uniquely) to MB.

A prime example of a category of coalgebras for an endofunctor on a category different from Set is the category DGF of descriptive general frames and appropriate morphisms. This is isomorphic to the category of coalgebras for the Vietoris functor V on Stone, the category of Stone spaces and continuous functions [START_REF] Kupke | Stone coalgebras[END_REF]. We recall the definition of the Vietoris functor on Top (originally introduced by Leopold Vietoris for compact Hausdorff spaces [START_REF] Vietoris | Bereiche zweiter Ordnung[END_REF], see also [START_REF] Johnstone | Stone Spaces. Cambridge Studies in Advanced Mathematics[END_REF]Section III.4] for a localic perspective), which restricts to the Vietoris functor V on Stone. Definition 2.7. For a topological space X let V X be the set of compact subsets of X topologized by

a = {b ∈ V X | b ⊆ a}, a = {b ∈ V X | b ∩ a = ∅},
where a ranges over the open sets of X. This is called the Vietoris topology. For a continuous function f :

X → X define V f : V X → V X : c → f [c], i.e. V f
is the direct image of f . Then V defines a functor on Top called the Vietoris functor.

It is well known that V restricts to an endofunctor on Stone, which we denote by V. Moreover, if X is a Stone space then the topology on VX is generated by a, a, where a ranges over the clopen subsets of X. The fact that V is the (Stone) dual of M then implies

MA ∼ = Alg(M) ≡ op Coalg(V) ∼ = DGF,
where we use ∼ = to indicate an isomorphism of categories and ≡ op for a dual equivalence. For details we refer to [START_REF] Kupke | Stone coalgebras[END_REF].

BAIOs and general frames

In this section we define boolean algebras with instantial operators (BAIOs) and general INL-frames.

A boolean algebra with instantial operators comprises of a boolean algebra B and an ω-indexed family of functions, reflecting the infinite number of modal operators in INL, and provide algebraic semantics for instantial neighbourhood logic. They play the same rôle for INL that modal algebras play for normal modal logic [START_REF] Chagrov | Modal Logic[END_REF][START_REF] Blackburn | Modal Logic. Cambridge Tracts in Theoretical Computer Science[END_REF] and boolean algebras with monotone operators for monotone modal logic [START_REF] Hansen | Monotonic modal logics[END_REF][START_REF] Hansen | A coalgebraic perspective on monotone modal logic[END_REF].

A general INL-frame is an INL-frame together with a collection of "admissible subsets" which is closed under certain operations. As usual, these admissible subsets form a BAIO. In the converse direction, we will show that every BAIO gives rise to a general INL-frame. Definition 3.1. A boolean algebra with instantial operators is a pair (B, (f n ) n∈ω ) consisting of a boolean algebra B and an ω-indexed set of functions f n : B n+1 → B satisfying the following equations for all n ∈ ω:

(B 1 ) f n (a 1 , . . . , a n-1 , ⊥; b) = ⊥; (B 2 ) f n (a 1 , . . . , a i , a i+1 , . . . , a n ; b) = f n (a 1 , . . . , a i+1 , a i , . . . , a n ; b); (B 3 ) f n (a 1 , . . . , a n ; b) ≤ f n (a 1 , . . . , a n ∨ a n ; b ∨ b ); (B 4 ) f n (a 1 , . . . , a n ; b) ≤ f n (a 1 , . . . , a n ∧ b; b); (B 5 ) f n (a 1 , . . . , a n ; b) ≤ f n+1 (a 1 , . . . , a n , c; b) ∨ f n (a 1 , . . . , a n ; b ∧ ¬c); (B 6 ) f n+1 (a 1 , . . . , a n+1 ; b) ≤ f n (a 1 , . . . , a n ; b); (B 7 ) f n (a 1 , . . . , a n ; b) ≤ f n+1 (a 1 , . . . , a n , a n ; b). A morphism between BAIOs (B, (f n ) n∈ω ) and (B , (f n ) n∈ω ) is a boolean algebra homomorphism h : B → B which satisfies h(f n (a 1 , . . . , a n ; b)) = f n (ha 1 , . . . , ha n ; hb)
for all a i , b ∈ B and n ∈ ω. The collection of BAIOs and BAIO morphisms forms a category (a variety of algebras, in fact) denoted by BAIO.

Every INL-frame (X, N ) gives rise to a BAIO, namely its complex algebra.

Example 3.2. Let (X, N ) be an INL-frame. Let PX be the powerset of X viewed as a boolean algebra and define f n (a 1 , . . . , a n ; b) = m (a 1 , . . . , a n ; b). Then it is easy to verify that (PX, (f n ) n∈ω ) is a BAIO. This is called the complex algebra of (X, N ). One can now ask whether G-INL can be restricted to a category of descriptive INL-frames such that the restriction of F to these descriptive frames gives rise to a dual equivalence with BAIO. This turns out to be the case for the following definition of descriptive INL-frames:

(PX) n+1 → PX (see Definition 2.3). A general INL-morphism from (X, N, A) to (X , N A ) is an INL-morphism f : (X, N ) → (X , N ) satisfying f -1 (a ) ∈ A for all a ∈ A . Write G-INL
Definition 3.7. A general INL-frame (X, N, A) is called:
differentiated if for any two distinct points x, y ∈ X there is a ∈ A such that

x ∈ a and y / ∈ a; The notion of crowdedness is the INL analogue of the tightness condition for normal modal logic [START_REF] Blackburn | Modal Logic. Cambridge Tracts in Theoretical Computer Science[END_REF]Definition 5.65]. Intuitively, it states that N (x) is, in a sense, determined by the admissible subsets. In passing, we make the following observation, the proof of which is straightforward. Proposition 3.8. Let (X, N ) be an INL-frame and suppose X is finite. Then A = PX is the unique set of admissible sets making (X, N, A) a descriptive INL-frame.

-compact if A = ∅ for
We aim to prove the following duality result: Theorem 3.9. We have a dual equivalence

D-INL ≡ op BAIO.
In order to prove this, we adhere to the strategy suggested in the introduction. First we identify BAIO with the category of algebras for some functor I on BA,

Concretely, the dual equivalence from Theorem 3.9 will be given by the construction from Example 3.6 and the subsequent paragraph, see Remark 5.7 below.

Duality

We show that BAIOs are algebras for the functor I : BA → BA, and that I is the (Stone) dual of the double Vietoris functor VV on Stone. As a consequence we obtain an algebra/coalgebra duality in Theorem 4.12. The assignment I determines an endofunctor on BA, called the instantial functor.

Item I 2 of Definition 4.1 allows us to put the a i in any desired order. In I 4 equality holds because of I 3 and in I 7 equality hold because of I 6 . The proof of the following theorem is standard.

Theorem 4.2. BAIO = Alg(I).

As stated in the introduction, it seems reasonable to expect that the double Vietoris functor VV is the dual of I under the dual equivalence between boolean algebras and Stone spaces. We prove that this is indeed the case. More concretely, we give a natural isomorphism

uf • I • clp → VV. (2)
We first work towards an isomorphism uf • I • clpX ∼ = VVX, where X is a Stone space. Lemma 4.11 then states that the collection of these isomorphisms is in fact natural. This ultimately proves the duality between (the categories of) I-algebras and VV-coalgebras (Theorem 4.12). We commence by giving an alternative subbase for the double Vietoris topology, which is tailored to our specific needs.

; b) = ( a 1 ∩ • • • ∩ a n ∩ b) and (a 1 , . . . , a n ; b) = ( a 1 ∪ • • • ∪ a n ∪ b).
In order to show that they are a subbase for the topology on VVX, we must show that A and A are boolean combinations of clopens of the form (a; b) and (a; b), where A is clopen in VX. Note that A can be written as the finite intersection of finite unions of clopens in VX of the form a, a. Moreover, we may assume that there is a single diamond in each finite union because diamonds distribute over unions. So we may write A = n i=1

a 1 ∪ • • • ∪ a mi ∪ b i . This implies A = n i=1 a 1 ∪ • • • ∪ a mi ∪ b i = n i=1 (a 1 , . . . , a mi ; b i ).
Similarly, writing A as a finite union of finite intersections, A can be expressed as a finite union of clopens of the form (a 1 , . . . , a n ; b).

We note that the statement of Proposition 4.3 holds for any topological space X if we require the a i and b to be range over the open subsets of X. The proof of this is slightly more involved because it crucially uses compactness of the elements of VX.

Remark 4.4. Recall that ultrafilters correspond bijectively to homomorphisms into 2, the two-element boolean algebra. For an ultrafilter u in B let p : B → 2 be the corresponding homomorphism. Then p(b) = iff b ∈ u. We will use these two perspectives interchangeably.

We now define a map ξ : uf • I • clpX → VVX, where X is a Stone space. These will form the components of the intended natural transformation from [START_REF] Van Benthem | A propositional dynamic logic for instantial neighbourhood semantics[END_REF]. Although such a map can be defined for any Stone space X, and therefore the definition actually yields a Stone-indexed collection of maps (ξ X ) X∈Stone , we shall refrain from writing this subscript until Theorem 4.11, where we prove that this collection is a natural transformation.

Intuitively, to an ultrafilter p we want to attach a closed subset W p of VX that satisfies W p ∈ (a 1 , . . . , a n ; b) if and only if p( (a 1 , . . . , a n ; b)) = . In our definition, we guarantee the implication from left to right by "killing the witnesses": If p( (a 1 , . . . , a n ; b)) = ⊥, then we make sure that none of the witnesses of (a 1 , . . . , a n b) is in W p . In other words, we stipulate that W p be disjoint from

a 1 ∩ • • • ∩ a n ∩ b.
W p = VX \ { a 1 ∩ • • • ∩ a n ∩ b | p( (a 1 , . . . , a n ; b)) = ⊥}.
Since W p is the complement of a union of clopen subsets of VX, it is closed in VX, hence an element of VVX. Therefore ξ is well defined. For the converse direction we need the following definition. Proof. In order to show that θ is well defined, we need to show that p W is an ultrafilter, that is, a boolean algebra homomorphism I • clpX → 2. Since I is defined by generators and relations it suffices to show that the images of the generators under p W satisfy the relations I 1 through I 7 . We leave this straightforward verification to the reader.

The following lemma provides the key ingredient for proving that ξ and θ are continuous and inverses of each other. The collection of witnesses is the set

A = a 1 ∩ • • • ∩ a n ∩ b
. This is a closed set of VX, and it is covered by the collection

{ c w,1 ∩ • • • ∩ c w,mw ∩ d w | w ∈ A}.
Clearly this set is an open covering of A, so by compactness of VX there must be a finite subcover of A. That is

A ⊆ w∈A ( c w,1 ∩ • • • ∩ c w,mw ∩ d w ),
where A is some finite subset of A serving as an index. Now it follows from Lemma 4.9 below that p( (a; b)) = ⊥.

The following technical result is motivated by the proof of Lemma 4.8. Lemma 4.9. Let X be a Stone space,

a i , b, c j , d ∈ clpX. Suppose A = a 1 ∩• • •∩ a n ∩ b is covered by the finite set {C i = c i,1 ∩• • •∩ c i,ni ∩ d i | 1 ≤ i ≤ m}. Suppose p : I • clpX → 2 is a point and p( (c i,1 , . . . , c i,ni ; d i )) = ⊥ for all C i in the given cover. Then p( (a 1 , . . . , a n ; b)) = ⊥.
Proof. If A = ∅ the lemma is trivial, so henceforth we shall assume A = ∅.

Part 1. Since (clearly) b ∈ A there must be a C i containing b. Call this C = c 1 ∩ • • • ∩ c k ∩ d. Now consider b j := b \ c j . This is not in C. If it is not in A, then we must have c j ⊇ a i for some i, because clearly b j ⊆ b. If it is in A, then it must be in another element of the cover, say, C j = c j1 ∩ • • • ∩ c jnj ∩ d j . Observe that b j = b \ c j ⊆ d j .
Next, consider b j,k := b \ (c j ∪ c jk ), where 1 ≤ k ≤ n j . If this is not in A, then we must have a i ⊆ c j ∪ c jk for some i. If it is in A, then it must be in one of the elements of the cover, say,

C jk = c jk,1 ∩ • • • ∩ c jk,n jk ∩ d jk .
Note that b j,k is not in C and not in C j by construction. Again, observe that b j,k ⊆ d jk . Continuing this way gives a tree, see the diagram below for intuition.

Each b j1,j2,...,

j k = b \ (c j1 ∪ c j1j2 ∪ • • • ∪ c j1j2•••j k
) is in none of the preceding cover elements. Since we started with a finite cover, this process must terminate, i.e. the branches of our tree must be finite. That is, at some point b j1,j2,...,j k is not in A, and since clearly b j1,j2,...,j k ⊆ b, it must be the case that b j1,j2,...,j k / ∈ a i for some a i , i.e. we must have

a i ⊆ (c j1 ∪ c j1j2 ∪ • • • ∪ c j1j2•••j k ).
Part 2. Now we have set ourselves up for the proof of the proposition. We will use rule I 5 finitely many times. The first step is:

(a; b) ≤ (a, c 1 ; b) ∨ (a; b \ c 1 ). ( 3
)
We continue using I 5 as follows: given an element of the form (a, c; b j1,j2,...,j k ) we verify what is the lowest entry such that c j1j2•••j k is not in c, and apply I 5 using this. It can be seen that ( 3) above is also obtained in this way. Thus the first two iterations are:

(a; b) ≤ (a, c 1 ; b) ∨ (a; b \ c 1 ) ≤ (a, c 1 , c 2 ; b) ∨ (a, c 1 ; b 2 ) ∨ (a, c 11 ; b 1 ) ∨ (a; b 1,11 )
For an entry, we cannot proceed if either all c j1•••j k , from a C j1•••j k in the tree already occur in c, or if the thing we subtract from b, i.e.

c j1 ∪c j1j2 ∪• • •∪c j1j2•••j k b C b1 = b \ c1 b2 = b \ c2 C1 C2 b1,1 = b \ (c1 ∪ c11) b1,2 = b \ (c1 ∪ c12) b2,1 = b \ (c2 ∪ c21) b2,2 = b \ (c2 ∪ c22) C11 C12 C21 C22
contains one of the a i (for then c j1j2•••j k , is not defined). In the first case, we have

(a, c; b \ (c j1 ∪ c j1j2 ∪ • • • ∪ c j1j2•••j k )) ≤ (c j1•••j k ,1 , . . . , c j1•••j k ,nj 1 •••j k ; d j1•••j k ). (4)
The inequality follows from using I 6 a lot, and applying I 3 to the fact that b j1,j2,...,j k ⊆ d j1•••j k . As the right hand side of ( 4) is one of the elements in the cover, we get

p( (a, c; b \ (c j1 ∪ c j1j2 ∪ • • • ∪ c j1j2•••j k ))) ≤ p( (c j1•••j k ,1 , . . . , c j1•••j k ,nj 1 •••j k ; d j1•••j k )) = ⊥.
In the second case, we get ⊥ because the intersection of one of the a i and b j1j2•••j k is empty, and we use I 4 and I 1 . Since this procedure is finite, this yields (a; b) ≤ ⊥, as desired.

As a corollary of Lemma 4.8 we obtain the following lemma. ) is an (n + 1)tuple of clopen subsets of X. We have

θ -1 (a; b) = θ -1 ({p | p( (a; b)) = }) = {W ∈ VVX | W ∈ (a; b)} = (a; b), which is clopen in VVX. Similarly ξ -1 ( (a; b)) = {p | W p ∈ (a; b)} = (a; b) .
We now show prove ξ • θ and θ • ξ are identities. For the former, observe that Lemma 4.8 implies p( (a; b)) = iff W p ∈ (a; b) iff p Wp ( (a; b)) = . So p and p W coincide on the generators of I(clpX), therefore p = p Wp and hence

θ • ξ = id uf•I•clpX .
To see that ξ • θ = id VVX , note that it suffices to show that W and W p W are in the same generating opens of the topology. Since the diamond is dual to the box it suffices to show that W / ∈ (a; b) iff W p W / ∈ (a; b). This is easy:

W / ∈ (a; b) iff p W ( (a, b)) = ⊥ iff W p W / ∈ (a; b).
The first "iff" holds by definition of θ, the second by Lemma 4.8.

Each Stone space X gives rise to a homeomorphism ξ, so we get a transformation (ξ X ) X∈Stone : uf • I • clp → VV. This transformation is in fact natural:

Lemma 4.11. The collection ξ = (ξ X ) X∈Stone : uf • I • clp → VV is a natural isomorphism.
Proof. We have already seen that ξ X is a homeomorphism for every Stone space X (i.e. an isomorphism in Stone), so it is left to show naturality. That is, where f : X → X is a continuous function we need to show that

uf • I • clpX VVX uf • I • clpX VVX ξ X uf•I•clpf VVf ξ X
commutes. Since elements of a Stone space are uniquely determined by the clopen sets in which they are contained, it suffices to show that for all p ∈ uf • I • clpX and a i , b ∈ clpX we have

VVf (ξ X (p)) ∈ (a; b) iff ξ X (uf • I • clpf (p)) ∈ (a; b).
This follows from a straightforward computation:

VVf (ξ X (p)) ∈ (a; b) iff ξ X (p) ∈ (VVf ) -1 ( (a; b)) iff ξ X (p) ∈ (f -1 a; f -1 b) iff p( (f -1 a; f -1 b)) = iff p(I • clpf ( (a; b))) = iff uf • I • clpf (p)( (a; b)) = iff ξ X (uf • I • clpf (p)) ∈ (a; b)
We conclude that (ξ X ) X∈Stone is indeed a natural isomorphism.

As an immediate corollary we obtain the main theorem of this section.

Theorem 4.12. We have a dual equivalence

Alg(I) ≡ op Coalg(VV).
As V is dual to the functor M on boolean algebras, we obtain the following corollary which confirms the intuition that INL is "modal logic taken twice". Corollary 4.13. The functor I is naturally isomorphic to the composition M•M. Lemma 5.6. Let (X, N, A) be a descriptive INL-frame, write X for the set X topologized by the clopen subbase A and let γ N :

X → VVX : x → {c ∈ VX | c ∈ N (x)}. Then (X, γ N ) is a VV-coalgebra.
Proof. The topological space X is zero-dimensional because A is closed under complementation (hence is a clopen base). Moreover, X is compact Hausdorff because (X, N, A) is compact and differentiated, so X is a Stone space.

In order to show that γ N is well defined, we need to show that γ N (x) is a closed subset of VX for every x ∈ X. Suppose c ∈ VX and c / ∈ γ N (x). Then c / ∈ N (x), and because (X, N, A) is crowded we can find (a 1 , . . . , a n ; b) which is witnessed by c but by none of the elements in N (x). This implies c ∈ a

1 ∩ • • • ∩ a n ∩ b and a 1 ∩ • • • ∩ a n ∩ b is disjoint from γ N (x). Thus we have found an open neighbourhood of c disjoint from γ N (x) so γ N (x) is closed in VX.
For continuity of γ N , it suffices to show that γ -1 N ( (a 1 , . . . , a n ; b)) is clopen in X for all a 1 , . . . , a n , b ∈ A. This is a consequence of the fact that A is closed under m , because γ -1 N ( (a 1 , . . . , a n ; b)) = m (a 1 , . . . , a n ; b).

We conclude that (X, γ N ) is a VV-coalgebra.

We proceed with the proof of Theorem 5.1.

Proof of Theorem 5.1. First we verify that the assignments from Lemmas 5.5 and 5.6 define a bijection between descriptive INL-frames and VV-coalgebras. Let (X, γ) be a VV-coalgebra. Lemma 5.5 assigns to this the descriptive INLframe (X, N γ , clpX). We know that the topology on X generated by clpX yields the topological space X, so applying Lemma 5.6 to (X, N γ , clpX) yields the VVcoalgebra (X, γ Nγ ). Furthermore, for a closed set c ∈ VX we have c ∈ γ Nγ (x) iff c ∈ N γ (x) iff c ∈ γ(x), hence γ = γ Nγ and (X, γ) = (X, γ Nγ ).

Conversely, suppose given a descriptive INL-frame (X, N, A). Write τ A for the topology on X generated by the (clopen) base A and let X = (X, τ A ). Then Lemma 5.6 sends (X, N, A) to (X, γ N ), which is in turn send to (X, N γ N , clpX) by Lemma 5.5. We know that the clopen sets of τ A are precisely the sets in A, so clpX = A. Comparing the neighbourhood functions gives

d ∈ N (x) iff d ∈ N (x) (Lemma 5.4) iff d ∈ γ N (x) (Lemma 5.6) iff d ∈ N γ N (x) (Lemma 5.5) iff d ∈ N γ N (x) (Lemma 5.4)
and therefore (X, N, A) = (X, N γ N , clpX). This proves the isomorphism on objects. Let (X, γ) and (X , γ ) be two VV-coalgebras and f : X → X a function. We claim that f is a VV-coalgebra morphism if and only if it is a general INLmorphism. If f is a general INL-morphism then clearly it is continuous. Since it is an INL-morphism moreover the diagram

X X PPX PPX f Nγ N γ PPf (5)
commutes. It follows immediately that

X X VVX VVX f γ γ VVf (6)
commutes, so f is an VV-coalgebra morphism.

Conversely, if f is continuous and ( 6) commutes, then (5) commutes because

d ∈ N γ (f (x)) iff d ∈ N γ (f (x)) iff d ∈ γ (f (x)) iff d ∈ VVf (γ(x)) iff d ∈ PPf (N γ (x)) iff d ∈ PPf (N γ (x)
). The last "iff" follows from Lemma 5.4. It is a general INL-morphism because continuity implies that f -1 sends admissible subsets to admissible subsets.

We have now completed the strategy outlined in diagram [START_REF] Van Benthem | A new game equivalence, its logic and algebra[END_REF]. As a corollary we obtain Theorem 3.9, whose formulation we copy here for the reader's convenience. Theorem 3.9. We have a dual equivalence D-INL ≡ op BAIO. Remark 5.7. Careful inspection of the definitions shows that the duality in Theorem 3.9 is given on objects by the construction in Example 3.6 and the subsequent paragraph.

Applications

We will give two applications of our results for completeness of INL-based logic and theory of INL-bisimulations.

Completeness

An extension of INL is any set of INL-formulas which contains INL (that is, all the INL-formulas valid on all INL-frames) and is closed under the rules of Modus Ponens and (RE). The latter states that for formulas α, β and ϕ, if α ↔ β, then ϕ[α/β] holds, where ϕ[α/β] is the result of possibly replacing some occurrences of α in ϕ by β (see [START_REF] Van Benthem | Instantial neighbourhood logic[END_REF]).

It is well known that every modal logic is sound and complete with respect to its algebraic semantics [START_REF] Chagrov | Modal Logic[END_REF][START_REF] Blackburn | Modal Logic. Cambridge Tracts in Theoretical Computer Science[END_REF][START_REF] Kupke | Algebraic semantics for coalgebraic logics[END_REF]. From the main completeness result of [START_REF] Van Benthem | Instantial neighbourhood logic[END_REF] it follows that BAIOs provide an algebraic semantics for INL. Then the standard argument yields that every extension L of INL is sound and complete with respect to the class of BAIOs validating L. Moreover, as a direct corollary of Theorem 3.9, we obtain: Theorem 6.1. Every extension of INL is sound and complete with respect to descriptive INL-frames.

Bisimulations

We briefly discuss bisimulations for INL and derive a Hennessy-Milner property for descriptive INL-frames. We work in a setting without proposition letters, but all results carry over to the setting with proposition letters.

Recall the definition of a bisimulation, in its coalgebraic form:

(Z, M ) (X , N ) f f
is a cospan in INL (witnessing behavioural equivalence of some states), then the pullback of f and f in Set is a bisimulation.

Define bisimulations between descriptive frames as follows: Definition 6.3. A descriptive INL-bisimulation between (X, γ) and (X , γ ) is a subspace B ⊆ X × X such that B is a bisimulation between the underlying neighbourhood frames.

In [START_REF] Enqvist | Bisimulations for coalgebras on Stone spaces[END_REF] the notion of Λ-bisimulation is introduced, where Λ is a so-called (characteristic) modal signature for an endofunctor on Stone. It is straightforward to see that the interpretation of INL in descriptive INL-frames can be translated to the setting used in op. cit. Moreover, an easy computation shows that every descriptive INL-bisimulation in the sense of Definition 6.3 is a Λ-bisimulation. We expect that the converse holds as well but at present do not have a proof of this. We leave it as an interesting open question.

We now prove a Hennessey-Milner property for descriptive INL-frames. This is the INL analogue of [5, Corollary 3.9]. Theorem 6.4. Let (X, γ) and (X , γ ) be descriptive frames. Then x ∈ X and x ∈ X are logically equivalent iff they are behaviourally equivalent iff they are linked by a descriptive INL-bisimulation.

Proof. Logical equivalence implies behavioural equivalence because every two logically equivalent states are identified by the theory map to the canonical model (i.e. the final object in D-INL). If x and x are behaviourally equivalent then there are morphisms in D-INL such that f (x) = f (x ). The pullback of f and f viewed as functions in Set is a bisimulation between the underlying neighbourhood frames (by the text following Definition 6.2). Moreover, this pullback is closed in X × X because pullbacks in Stone are computed as in Set. Hence behavioural equivalence implies bisimilarity. Lastly, bisimilarity implies logical equivalence by design.

We can apply this theorem to all INL-frames that carry a descriptive structure, that is, to (X, N ) ∈ INL such that there exists A making (X, N, A) a descriptive INL-frame. Corollary 6.5. Suppose the INL-frames (X, N ) and (X , N ) both carry a descriptive structure. Then between these frames, bisimilarity coincides with logical equivalence.

Restricting this corollary entails [3, Theorem 3.1], the Hennessy-Milner property for finite frames, because all finite neighbourhood frames carry a descriptive frame structure (see Proposition 3.8). Theorem 6.6. Let (X, N ) and (X , N ) be finite neighbourhood frames. Then bisimilarity coincides with logical equivalence.

Conclusion and future work

In this paper we introduced descriptive frames for the Instantial Neighbourhood Logic (INL) and showed that these frames are dual to BAIOs, the algebras for INL. Coalgebra provided a key for obtaining this duality. We first presented BAIOs as algebras for the functor I on the category of boolean algebras. We also represented descriptive INL-frames as coalgebras for the double Vietoris functor VV on the category of Stone spaces. Finally, we showed that the category of Ialgebras is dual to the category of VV-coalgebras, leading to the desired duality result. As a corollary we obtained that every extension of INL is sound and complete with respect to descriptive INL-frames. One interesting question for future work is whether one can obtain an analogue of the celebrated Sahlqvist completeness and correspondence result for extensions of INL.

We recall that the Vietoris functor V is dual to the functor M on the category of boolean algebras (Section 2). Intuitively M freely adds one layer of normal modalities to a boolean algebra. We showed in this paper that BAIOs can be represented as algebras for M • M (Section 4). Therefore, BAIOs can be seen as "modal algebras squared" and INL itself is, in a way, "the basic modal logic squared". This provokes the question of what "modal algebras cubed" looks like, i.e. what logic and algebras correspond to the functor M • M • M, and similar questions for the n-fold composition of M.

Recall that monotone neighbourhood logic EM algebraically corresponds to a functor N on boolean algebras which intuitively adds one layer of monotone modalities to a boolean algebra [START_REF] Hansen | Monotonic modal logics[END_REF][START_REF] Hansen | A coalgebraic perspective on monotone modal logic[END_REF]. This generates a question whether NNalgebras and the corresponding logic admit an "INL-style axiomatization".

Another related formalism that would be interesting to investigate is that of positive INL. The algebras for this logic are distributive lattices with instantial operators (DLIOs): These are of course algebras for a endofunctor J on the category DL of distributive lattices and homomorphisms. In analogy with the results of this paper, one would expect that descriptive frames for positive INL are isomorphic to coalgebras for the double convex Vietoris functor V c on the category of Priestley spaces, as this is the Priestley space analogue of the Vietoris functor [START_REF] Palmigiano | A coalgebraic view on positive modal logic[END_REF][START_REF] Bezhanishvili | Free modal algebras: A coalgebraic perspective[END_REF][START_REF] Venema | Modal logic and the Vietoris functor[END_REF]. We expect the following duality result: If correct, this may also provide a novel algebraic presentation of the double Vietoris powerlocale studied extensively by Vickers [START_REF] Vickers | The double powerlocale and exponentiation: A case study in geometric logic[END_REF][START_REF] Vickers | A universal characterization of the double powerlocale[END_REF][START_REF] Vickers | Constructive points of powerlocales[END_REF].

Definition 2 . 3 .

 23 Let (X, N ) be a neighbourhood frame. Define the map m ,n : (PX) n+1 → PX by m ,n (a 1 , . . . , a n ; b) = {x ∈ X | ∃w ∈ N (x) which witnesses (a 1 , . . . , a n ; b)}.

Example 3 . 3 .

 33 Recall that Prop is an arbitrary but fixed set of proposition letters and let L = L(Prop) be the collection of instantial formulas as defined in Subsection 2.1. Write ϕ ≡ ψ if two formulas are provably equivalent in the axiomatization given in [3, Section 4] and write [ϕ] for the equivalence class of ϕ under ≡. Then L/≡ is a BAIO, where f n ([ϕ 1 ], . . . , [ϕ n ]; [ψ]) is defined to be [ (ϕ 1 , . . . , ϕ n ; ψ)]. This is of course the free BAIO generated by Prop, and is known as the Lindenbaum-Tarski algebra.Towards a duality theorem for BAIOs, we define general INL-frames. These are INL-frames together with a subalgebra of their complex algebra. Definition 3.4. A general INL-frame is a triple (X, N, A) such that (X, N ) is an INL-frame and A ⊆ PX is a collection of admissible sets that is closed under boolean operations and the operation m :

  for the category of general INL-frames and general INL-morphisms. Since every algebra is a subalgebra of itself, every INL-frame can be seen as a general INL-frame: Example 3.5. If (X, N ) is an INL-frame, then setting A = PX yields a general INL-frame. Example 3.6. For a BAIO (B, (f n ) n∈ω ), let ufB be the collection of ultrafilters of B and let B = { a | a ∈ B}, where a = {u ∈ ufB | a ∈ u}. Define a neighbourhood function N for ufB via N (u) = {d ⊆ ufB | f n (a 1 , . . . , a n ; b) ∈ u whenever d witnesses ( a 1 , . . . , a n ; b )}. Then (ufB, N, B) is a general INL-frame. In the converse direction of Example 3.6 we have the functor F : G-INL → BAIO which sends a general INL-frame (X, N, A) to (A, (m ,n ) n∈ω ).

  any subset A of A with the finite intersection property; crowded if for all x ∈ X and d ⊆ X such that d / ∈ N (x) we can find a 1 , . . . , a n , b such that d witnesses (a 1 , . . . , a n ; b) while no d ∈ N (x) witnesses (a 1 , . . . , a n ; b). A descriptive INL-frame is a general INL-frame that is differentiated, compact and crowded. Denote by D-INL the full subcategory of G-INL whose objects are descriptive INL-frames.

  then we determine the (Stone) dual of I, and finally, we show that descriptive INL-frames are precisely coalgebras for this dual functor. In a diagram:

Definition 4 . 1 .

 41 Let B be a boolean algebra. Abbreviate (a; b) = (a 1 , . . . , a n ; b) for an (n + 1)-tuple of elements of B. Let IB be the boolean algebra generated by (a 1 , . . . , a n ; b), where n ∈ ω and a i , b ∈ B, subject to the relations (I 1 ) (a, ⊥; b) = ⊥; (I 2 ) (a 1 , . . . , a i , a i+1 , . . . , a n ; b) = (a 1 , . . . , a i+1 , a i , . . . , a n ; b); (I 3 ) (a, c; b) ≤ (a, c ∨ c , b ∨ b ); (I 4 ) (a, c; b) ≤ (a, c ∧ b; b); (I 5 ) (a; b) ≤ (a, c; b) ∨ (a; b ∧ ¬c); (I 6 ) (a, c; b) ≤ (a; b); (I 7 ) (a 1 , . . . , a n ; b) ≤ (a 1 , . . . , a n , a n ; b). For a homomorphism f : B → B define If : IB → IB on generators by (If )( (a 1 , . . . , a n ; b)) = (f (a 1 ), . . . , f (a n ); f (b)).

Proposition 4 . 3 .

 43 Let X be a Stone space. The topology on VVX is generated by the clopen subbase (a 1 , . . . , a n ; b) = {W ∈ VVX | ∃w ∈ W s.t. w witnesses (a 1 , . . . , a n ; b)}, (a 1 , . . . , a n ; b) = {W ∈ VVX | ∀w ∈ W w co-witnesses (a 1 , . . . , a n ; b)}, where the a i , b range over the clopen subsets of X. Proof. The given sets are clopen in VVX, because (a 1 , . . . , a n

Definition 4 . 5 .

 45 For a Stone space X, define ξ : uf • I • clpX → VVX by sending an ultrafilter p to

Definition 4 . 6 .Lemma 4 . 7 .

 4647 For a Stone space X, define θ : VVX → uf • I • clpX : W → p W , where p W : I(clpX) → 2 is given on generators by p W : I • clpX → 2 : (a; b) → if W ∈ (a; b) ⊥ otherwise The assignment θ is well defined.

Lemma 4 . 8 .

 48 Let X be a Stone space. We haveW p ∈ (a; b) if and only if p( (a; b)) = . Proof. If p( (a; b)) = ⊥, then by construction W p / ∈ (a; b). So suppose W p / ∈ (a, b).Then for every witness w of (a, b) there exists (c w , d w ) which is witnessed by w and is such that p( (c w , d w )) = ⊥.

Lemma 4 . 10 .

 410 The maps θ and ξ are continuous and each others inverses. Hence ξ is a homeomorphism. Proof. We first prove continuity. The open subsets of uf • I • clpX are generated by (a; b) = {p | p( (a; b)) = }, where (a; b) = (a 1 , . . . , a n ; b

Definition 7 . 1 .

 71 A distributive lattice with instantial operators (DLIO) is a tuple (D, (f n ) n∈ω , (g n ) n∈ω ) consisting of a distributive lattice D and two collections of ω-indexed maps f n , g n : D n+1 → D such that: (1) The f n satisfy (B 1 ) to (B 7 ) from Definition 3.1, where, in absence of negation, we reformulate (B 5 ) asf n (a 1 , . . . , a n ; b) ≤ f n+1 (a 1 , . . . , a n , c; b) ∨ f n (a 1 , . . . , a n ; b ∧ d), whenever c ∨ d = ;(2) The g n satisfy relations dual to the ones for f n ; and(3) The f n and g n satisfy the duality axiomsg n+1 (a 1 , . . . , a n , b ; b) ∧ m i=1 g n (a 1 , . . . , a n ; a i ∨ b) ≤ g n (a 1 , . . . , a n ; b) ∨ f m (a 1 , . . . , a m ; b ) (D 1) and f n (a 1 , . . . , a n ; b) ∧ g m (a 1 , . . . , a m ; b ) ≤ f n+1 (a 1 , . . . , a n , b ; b) ∨ m i=1 f n (a 1 , . . . , a n ; a i ∧ b).(D 2 )

Conjecture 7 . 2 .

 72 We have a dual equivalenceAlg(J) ≡ op Coalg(V c V c ).Finally, related to positive INL, an interesting question is to consider the geometric logic analogue of INL and to verify a slogan of[START_REF] Bezhanishvili | Coalgebraic Geometric Logic[END_REF], which in the case of INL will read as Geometric INL = Positive INL + Scott continuity.

Descriptive frames as coalgebras

We show that the descriptive frames from Definition 3.7 are precisely coalgebras for the double Vietoris functor VV. Proof. We show that d Proof. This follows directly from the proof of Lemma 5.3.

The following two lemmas describe the object part of the isomorphism from Theorem 5.1. Lemma 5.5. Let (X, γ) be a VV-coalgebra. Write X for the space underlying X and let

Proof. We know that clpX is closed under boolean operations and it follows from continuity of γ that clpX is closed under m . Furthermore, (X, N γ , clpX) is differentiated because X is Hausdorff and compact because X is compact.

Lastly, we show that it is crowded. Suppose c / ∈ N γ (x). Without loss of generality we may assume c to be closed, hence an element of VX, because we know from Lemma 5.3 that c and c witness precisely the same tuples. It follows from the definition of N γ that c / ∈ γ(x). Since γ(x) is a closed subset of VX, there must be a basic clopen a 1 ∩ • • • ∩ a n ∩ b containing c and disjoint from γ(x). Therefore c witnesses (a 1 , . . . , a n ; b) while none of the elements in γ(x) witness (a 1 , . . . , a n ; b). It then follows from the definition of N γ and Lemma 5.3 that none of the d ∈ N γ (x) witness (a 1 , . . . , a n ; b). Therefore (X, N γ , clpX) is crowded.


Bart Jacobs

Sam Staton
email: sam.staton@cs.ox.ac.uk

De Finetti's Construction as a Categorical Limit

This paper reformulates a classical result in probability theory from the 1930s in modern categorical terms: de Finetti's representation theorem is redescribed as limit statement for a chain of finite spaces in the Kleisli category of the Giry monad. This new limit is used to identify among exchangeable coalgebras the final one.

Introduction

An indifferent belief about the bias of a coin can be expressed in various ways. One way is to use elementary sentences like "When we toss the coin 7 times, the probability of 5 heads is 1 8 ." "When we toss the coin k times, the probability of n heads is 1 k+1 ."

Another way is to give a probability measure on the space [0, 1] of biases:

"The bias of the coin is uniformly distributed across the interval [0, 1]." [START_REF] Dahlqvist | Robustly parameterised higher-order probabilistic models[END_REF] This sentence (2) is more conceptually challenging than (1), but we may deduce (1) from (2) using Lebesgue integration: where k n = k! n!(k-n)! is the binomial coefficient. Here we have considered indifferent beliefs as a first illustration, but more generally de Finetti's theorem gives a passage from sentences about beliefs like [START_REF] Ackerman | Exchangeable random primitives[END_REF] to sentences like [START_REF] Dahlqvist | Robustly parameterised higher-order probabilistic models[END_REF].

Theorem 1 (De Finetti, Informal). If we assign a probability to all finite experiment outcomes involving a coin (such as (1)), and these probabilities are all suitably consistent, then by doing so we have given a probability measure on [0, 1] (such as the uniform distribution, (2)).

In this paper we give two categorical / coalgebraic formulations of this theorem.

-In Theorem 8, we state the result as: the unit interval [0, 1] is an inverse limit over a chain of finite spaces in a category of probability channels. In particular, a cone over this diagram is an assignment of finite probabilities such as [START_REF] Ackerman | Exchangeable random primitives[END_REF] that is suitably consistent. -In Theorem 12, we state the result as: [0, 1] carries a final object in a category of (exchangeable) coalgebras for the functor 2 × (-) in the category of probability channels. A coalgebra can be thought of as a process that coinductively generates probabilities of the form [START_REF] Ackerman | Exchangeable random primitives[END_REF]. A coalgebra is a little more data than strictly necessary, but this extra data corresponds to the concept of sufficient statistics which is useful in Bayesian inference.

Multisets and probability distributions. A multiset is a 'set' in which elements may occur multiple times. We can write such a multiset over a set {R, G, B}, representing red, green and blue balls, as:

3| R + 5|G + 2| B .
This multiset can be seen as an urn containing three red, five green and two blue balls.

A probability distribution is a convex combination of elements, where the frequencies (or probabilities) with which elements occur are numbers in the unit interval [0, 1] that add up to one, as in:

3 10 | R + 1 2 |G + 1 5 | B .
Obviously, distributions, whether discrete (as above) or continuous, play a central role in probability theory. Multisets also play a crucial role, for instance, an urn with coloured balls is very naturally represented as a multiset. Similarly, multiple data items in learning scenarios are naturally captured by multisets (see e.g. [START_REF] Jacobs | Structured probabilistic reasoning[END_REF]). The two concepts are related, since any multiset gives rise to a probability distribution, informally by thinking of it as an urn and then drawing from it (sampling with replacement). This paper develops another example of how the interplay between multisets and distributions involves interesting structure, in an emerging area of categorical probability theory.

Beliefs as cones. In brief, following an experiment involving K tosses of a coin, we can set up an urn that approximately simulates the coin according to the frequencies that we have seen. So if we see 5 heads out of 7 tosses, we put 5 black balls into an urn together with 2 white balls, so that the chance of black(=heads) is 5 7 . We can describe a belief about a coin by describing the probabilities of ending up with certain urns (multisets) after certain experiments. Clearly, if we draw and discard a ball from an urn, then this is the same as stopping the experiment one toss sooner. So a consistent belief about our coin determines a cone over the chain

M[1](2) M[2](2) • o o M[3](2) • o o . . . • o o (3)
in the category of finite sets and channels (aka probability kernels). Here M

[K](2)
is the set of multisets over 2 of size K, i.e. urns containing K balls coloured black and white, and the leftward arrows describe randomly drawing and discarding a ball. We use the notation → for channels, a.k.a. Kleisli map, see below for details. Our formulation of de Finetti's theorem says that the limit of this chain is [0, 1]. So to give a belief, i.e. a cone over (3), is to give a probability measure on [0, 1]. We set up the theory of multisets and cones in Section 3, proving the theorem in Section 6.

Exchangeable coalgebras. In many situations, it is helpful to describe a belief about a coin in terms of a stateful generative process, i.e. a channel (aka probability kernel) h : X → 2 × X, for some space X, which gives coinductively a probability for a sequence of outcomes. This is a coalgebra for the functor 2 × (-). An important example is Pólya's urn, which is an urn-based process, but one where the urn changes over time. Another important example puts the carrier set X = [0, 1] as the set of possible biases, and the process merely tosses a coin with the given bias. We show that [0, 1] carries the final object among the 'exchangeable' coalgebras. Thus there is a canonical channel X → [0, 1], taking the belief described by a generative process such as Pólya's urn to a probability measure on [0, 1] such as the uniform distribution. We set up the theory of exchangeable coalgebras in Section 4, proving the final coalgebra theorem in Section 7 by using the limit reformulation of de Finetti's theorem.

Background on mulitsets and distributions

Multisets. A multiset (or bag) is a 'set' in which elements may occur multiple times. We shall write M(X) for the set of (finite) multisets with elements from a set X. Elements ϕ ∈ M(X) may be described as functions ϕ : X → N with finite support, that is, with supp(ϕ) := {x ∈ X | ϕ(x) = 0} is finite. Alternatively, multisets can be described as formal sums i n i |x i , where n i ∈ N describes the multiplicity of x i ∈ X, that is, the number of times that the element x i occurs in the multiset. The mapping X → M(X) is a monad on the category Sets of sets and functions. In fact, M(X) with pointwise addition and empty multiset 0, is the free commutative monoid on X.

Frequently we need to have a grip on the total number of elements occurring in a multiset. Therefore we write, for K ∈ N,

M[K](X) := {ϕ ∈ M(X) | ϕ has precisely K elements} = {ϕ ∈ M(X) | x∈X ϕ(x) = K}.
Clearly, M[0](X) is a singleton, containing only the empty multiset 0. Each M[K](X) is a quotient of the set of sequences X K via an accumulator map:

X K acc X / / M[K](X) with acc X (x 1 , . . . , x K ) := x∈X i 1 xi (x) x (4)
where 1 xi is the indicator function sending x ∈ X to 1 if x = x i and to 0 otherwise. In particular, for

X = 2, acc 2 (b 1 , . . . , b K ) = ( i b i )| 1 + (K -i b i )| 0 .
The map acc X is permutation-invariant, in the sense that:

acc X (x 1 , . . . , x K ) = acc X (x σ(1) , . . . , x σ(K) )
for each permutation σ ∈ S K .

Such permutation-invariance, or exchangeability, plays an important role in de Finetti's work [START_REF] De Finetti | Funzione caratteristica di un fenomeno aleatorio[END_REF], see the end of Section 7.

Discrete probability. A discrete probability distribution on a set X is a finite formal sum i r i | x i of elements x i ∈ X with multiplicity r i ∈ [0, 1] such that i r i = 1. It can also be described as a function X → [0, 1] with finite support. We write D(X) for the set of distributions on X. This gives a monad D on Sets; it satisfies D(1) ∼ = 1 and D(2) ∼ = [0, 1], where 1 = {0} and 2 = {0, 1}.

Maps in the associated Kleisli category K (D) will be called channels and are written with a special arrow →. Thus f : X → Y denotes a function f : X → D(Y ). For a distribution ω ∈ D(X) and a channel g : Y → Z we define a new distribution f = ω ∈ D(Y ) and a new channel g • • f : X → Z by Kleisli composition:

f = ω := y∈Y x ω(x) • f (x)(y) y g • • f (x) := g = f (x).
Discrete probability over multisets. For each number K ∈ N and probability r ∈ [0, 1] there is the familiar binomial distribution binom[K](r) ∈ D({0, 1, . . . , K}).

It captures probabilities for iterated flips of a known coin, and is given by the convex sum:

binom[K](r) := 0≤k≤K K k • r k • (1 -r) K-k k .
The multiplicity probability before | k in this expression is the chance of getting k heads of out K coin flips, where each flip has fixed bias r ∈ [0, 1]. In this way we obtain a channel binom[K] : [0, 1] → {0, 1, . . . , K}. More generally, one can define a multinomial channel:

D(X) • mulnom[K] / / M[K](X).
It is defined as:

mulnom[K](ω) := ϕ∈M[K](X) K! x ϕ(x)! • x ω(x) ϕ(x) ϕ .
The binomial channel is a special case, since [0, 1] ∼ = D(2) and {0, 1, . . . , K} ∼

= M[K](2), via k → k| 0 + (K -k)| 1 .
The binary case will play an important role in the sequel.

Drawing from an urn

Recall our motivation. We have an unknown coin, and we are willing to give probabilities to the outcomes of different finite experiments with it. From this we ultimately want to say something about the coin. The only experiments we consider comprise tossing a coin a fixed number K times and recording the number of heads. The coin has no memory, and so the order of heads and tails doesn't matter. So we can imagine an urn containing black balls and white balls, and in an experiment we start with an empty urn and put a black ball in the urn for each head and a white ball for each tail. The urn forgets the order in which the heads and tails appear. We can then describe our belief about the coin in terms of our beliefs about the probability of certain urns occurring in the different experiments. These probabilities should be consistent in the following informal sense, that connects the different experiments.

-If we run the experiment with K + 1 tosses, and then discard a random ball from the urn, it should be the same as running the experiment with just K tosses.

In more detail: because the coin tosses are exchangeable, that is, the coin is memoryless, to run the experiment with K + 1 tosses, is to run the experiment with K + 1 tosses and then report some chosen permutation of the results. This justifies representing the outcome of the experiment with an unordered urn. It follows that the statistics of the experiment are the same if we choose a permutation of the results at random. To stop the experiment after K tosses, i.e. to discard the ball corresponding to the last toss, is thus to discard a ball unifomly at random. As already mentioned: an urn filled with certain objects of the kind x 1 , . . . , x n is very naturally described as a multiset i n i | x i , where n i is the number of objects x i in the urn. Thus an urn containing objects from a set X is a multiset in M(X). For instance, an urn with three black and two white balls can be described as a multiset 3|B + 2| W ∈ M(2), where B stands for black and W for white. We can thus formalise a belief about the K-th experiment, where we toss our coin K times, as a distribution ω K ∈ D(M[K](2)), on urns with K black and white balls.

For the consistency property, we need to talk about drawing and discarding from an urn. We define a channel that draws a single item from an urn:

M[K + 1](X) D / / D X × M[K](X) (5)
It is defined as:

D(ϕ) := x∈supp(ϕ) ϕ(x) y ϕ(y) x, ϕ -1| x .
Concretely, in the above example:

D 3| B + 2| W = 3 5 B, 2| B + 2| W + 2 5 W, 3| B + 1| W .
Notice that on the right-hand-side we use brackets | -inside brackets | -. The outer | -are for D and the inner ones for M.

We can now describe the 'draw-and-delete' channel, by post-composing D with the second marginal:

M[K + 1](X) DD := D(π2)•D / / D M[K](X) Explicitly, DD(ϕ) = x ϕ(x) y ϕ(y) ϕ -1| x .
Now the consistency property requires that the beliefs about the coin comprise a sequence of distributions

ω K ∈ D(M[K](2)) such that (DD = ω K+1 ) = ω K .
Thus they should form a cone over the sequence

M[0](2) M[1](2) • DD o o M[2](2) • DD o o . . . • DD o o M[K](2) • DD o o . . . • DD o o (6) This means that for all K, ω K (ϕ) = ϕ(B)+1 K+1 • ω K+1 (ϕ + | B ) + ϕ(W )+1 K+1 • ω K+1 (ϕ + | W ). ( 7
)
Known bias is a consistent belief. If we know for sure that the bias of a coin is r ∈ [0, 1], then we would put ω K = binom[K](r). This is a consistent belief, which is generalised in the following result to the multinomial case. This cone forms the basis for this paper.

Proposition 2. The multinomial channels form a cone for the chain of drawand-delete channels, as in:

M[0](X) • • • • DD o o M[K](X) • DD o o M[K + 1](X) • DD o o • • • • DD o o D(X) • mulnom[K] O O • mulnom[K+1] • • • : : • mulnom[0] f f (8)
Our reformulation of the de Finetti theorem explains the sense in which above cone is a limit when X = 2, see Theorem 8.

Proof. For ω ∈ D(X) and ϕ ∈ M[K](X) we have:

DD • • mulnom[K + 1] (ω)(ϕ) = ψ mulnom[K + 1](ω)(ψ) • DD[K](ψ)(ϕ) = x mulnom[K + 1](ω)(ϕ + 1|x ) • ϕ(x)+1 K+1 = x (K+1)! y (ϕ+1| x )(y)! • y ω(y) (ϕ+1| x )(y) • ϕ(x)+1 K+1 = x K! y ϕ(y)! • y ω(y) ϕ(y) • ω(x) = K! y ϕ(y)! • y ω(y) ϕ(y) • x ω(x) = mulnom[K](ω)(ϕ).
Unknown bias (uniform) is a consistent belief. If we do not know the bias of our coin, it may be reasonable to say that all the (K + 1) outcomes in M[K](2) are equiprobable. This determines the discrete uniform distribution

υ K ∈ D(M[K](2)), υ K := K k=0 1 K+1 k| B + (K -k)| W .
Proposition 3. The discrete uniform distributions υ K form a cone for the chain of draw-and-delete channels, as in:

M[0](X) • • • • DD o o M[K](X) • DD o o M[K + 1](X) • DD o o • • • • DD o o 1 • υ K O O • υ K+1 • • • 9 9 • υ0 f f (9) Proof. For ϕ ∈ M[K](2)
we have:

DD = υ K+1 (ϕ) = ψ υ K+1 (ψ) • DD[K](ψ)(ϕ) = υ K+1 (ϕ + |W ) • DD[K](ϕ + |W )(ϕ) + υ K+1 (ϕ + | B ) • DD[K](ϕ + |B )(ϕ) = 1 K+2 • ϕ(W )+1 K+1 + 1 K+2 • ϕ(B)+1 K+1 = ϕ(W )+ϕ(B)+2 (K+2)(K+1) = 1 K+1 since ϕ(W ) + ϕ(B) = K.

Coalgebras and Pólya's urn

In the previous section we have seen two examples of cones over the chain [START_REF] Feller | An Introduction to Probability Theory and Its applications[END_REF]: one for a coin with known bias (Proposition 2), and one where the bias of the coin is uniformly distributed (Proposition 3).

In practice, it is helpful to describe our belief about the coin in terms of a data generating process. This is formalised as a channel h : X → 2 × X, i.e. as a coalgebra for the functor 2 × (-) on the category of channels. The idea is that our belief about the coin is captured by some parameters, which are the states of the coalgebra x ∈ X. The distribution h(x) describes our belief about the outcome of the next coin toss, but also provides a new belief state according to the outcome. For example, if we have uniform belief about the bias of the coin, we predict the outcome to be heads or tails equally, but afterward the toss our belief is refined: if we saw heads, we believe the coin to be more biased towards heads.

Pólya's urn is an important example of such a coalgebra. We describe it as a multiset over 2 = {0, 1} with a certain extraction and re-fill operation. The number 0 corresponds to black balls, and 1 to white ones, so that a multiset ϕ ∈ M(2) captures an urn with ϕ(0) black and ϕ(1) white ones. When a ball of color x ∈ 2 is extracted, it is put back together with an extra ball of the same color. We choose to describe it as a coalgebra on the set M * (2) of non-empty multisets over 2. Explicitly, pol : M * (2) → 2 × M * (2) is given by:

pol(ϕ) := ϕ(0) ϕ(0) + ϕ(1) 0, ϕ + 1|0 + ϕ(1) ϕ(0) + ϕ(1) 1, ϕ + 1| 1 .
So the urn keeps track of the outcomes of the coin tosses so far, and our belief about the bias of the coin is updated according to successive experiments.

Iterating draws from coalgebras

By iterating a coalgebra h : X → 2 × X, we can simulate the experiment with

K coin tosses h K : X → M[K](2)
, by repeatedly applying h. Formally, we build a sequence of channels h K : X → M[K](2) × X by h 0 (x) := (0, x) and:

h K+1 := X • h K / / M[K](2) × X • id×h / / M[K](2) × 2 × X add×id / / M[K + 1](2) × X
where the rightmost map add :

M[K](2) × 2 → M[K + 1](2) is add(ϕ, b) = ϕ + 1|b .
(Another way to see this is to regard a coalgebra h : X → 2 × X in particular as coalgebra X → M(2) × X. Now M(2) × -is the writer monad for the commutative monoid M(2), i.e. the monad for M(2)-actions. Iterated Kleisli composition for this monad gives a sequence of maps h : X → M(2) × X.)

For example, starting with Pólya's urn pol : M * (2) → 2 × M * (2), we look at a few iterations:

pol 0 (b|0 + w| 1 ) = 1 0, b| 0 + w|1 pol 1 (b|0 + w| 1 ) = pol(b|0 + w| 1 ) = b b+w 1|0 , ϕ + | 0 + w b+w 1| 1 , ϕ + | 1 pol 2 (b|0 + w| 1 ) = b b+w • b+1 b+w+1 2|0 , (b + 2)| 0 + w| 1 + b b+w • w b+w+1 1| 0 + 1|1 , (b + 1)| 0 + (w + 1)|1 + w b+w • b b+w+1 1| 0 + 1|1 , (b + 1)| 0 + (w + 1)|1 + w b+w • w+1 b+w+1 2| 1 , b| 0 + (w + 2)|1 = b(b+a) (b+w)(b+w+1) 2|0 , (b + 2)| 0 + w| 1 + 2bw (b+w)(b+w+1) 1| 0 + 1|1 , (b + 1)| 0 + (w + 1)| 1 + w(w+1) (b+w)(b+w+1) 2| 1 , b| 0 + (w + 2)|1 .
(10) It is not hard to see that we get as general formula, for K ∈ N:

pol K (b| 0 + w| 1 ) = 0≤k≤K K k • i<k (b + i) • i<K-k (w + i) i<K (b + w + i) k|0 +(K -k)| 1 , (b+k)|0 + (w+(K -k))| 1 .
We are especially interested in the first component of h K (x), which is in M[K](2). Thus we define the channels:

h K := X h K • / / M[K](2) × X π1 / / M[K](2)
For the Pólya urn pol, the really remarkable fact about pol K : 2) is that if we start with the urn with one white ball and one black ball, these distributions on M[K](2) that come from iteratively drawing are uniform distributions:

M * (2) → M[K](
pol K (1|0 + 1| 1 ) = υ K .
More generally:

Proposition 4. pol K (b| 0 + w| 1 ) k| 0 + (K -k)| 1 = K k • (b + k -1)! (b -1)! • (w + K -k -1)! (w -1)! • (b + w -1)! (b + w + K -1)! . (11)
Proof. We start from the K-th iteration formula for pol, given just before Proposition 4, and derive:

i<k (b + i) • i<K-k (w + i) i<K (b + w + i) = (b + k -1)! (b -1)! • (w + K -k -1)! (w -1)! • (b + w -1)! (b + w + K -1)! .
From this characterization, we can deduce that the channels pol K : M * (2) → M[K](2) form a cone over the draw-and-delete chain (6), i.e. that DD • • pol K+1 = pol K , by a routine calculation.

In what follows we provide two other ways to see that pol K forms a cone. First we deduce it using the fact that the coalgebra pol is exchangeable (Lemma 6). Second we deduce it by noticing that pol K (b| 0 + w| 1 )(k|0 + (K -k)| 1 ) is distributed as betabin[K](b, w), the beta binomial distribution, and hence factors through the binomial cone (Proposition 2) via the beta channel (Lemma 7).

Exchangeable coalgebras and cones

We would like to focus on those coalgebras h : X → 2×X that describe consistent beliefs, i.e. for which h K : X → M[K](2) is a cone over the chain [START_REF] Feller | An Introduction to Probability Theory and Its applications[END_REF]:

DD • • h K+1 = h K . ( 12
)
For example, Pólya's urn forms a cone. But the deterministic alternating coalgebra

alt : 2 → 2 × 2 alt(b) := 1| b, ¬b (13)
does not form a cone, since for instance alt 1 (0) = 1| 0 , while

DD • • alt 2 (0) = 1 2 | 0 + 1 2 | 1 .
The following condition is inspired by de Finetti's notion of exchangeability, and gives a simple coinductive criterion for a coalgebra to yield a cone [START_REF] Jacobs | Structured probabilistic reasoning[END_REF]. It is also related to ideas from probabilistic programming (e.g. [START_REF] Ackerman | Exchangeable random primitives[END_REF]). Definition 5. A coalgebra h : X → 2 × X will be called exchangeable if its outputs can be reordered without changing the statistics, as expressed by commutation of the following diagram.

2 × X id⊗h • / / 2 × 2 × X swap×id X ∼ = X h • 0 0 h • . . 2 × X id⊗h • / / 2 × 2 × X (14)
Returning to Pólya's urn coalgebra pol : M * (2) → 2 × M * (2), we see that it is exchangeable, for, by a similar argument to [START_REF] Hausdorff | Summationsmethoden und Momentfolgen I[END_REF],

(id × pol)(pol(b| 0 + w|1 )) = = b b+w • b+1 b+w+1 (0, 0), (b + 2)| 0 + w| 1 + b b+w • w b+w+1 (0, 1), (b + 1)| 0 + (w + 1)| 1 + w b+w • b b+w+1 (1, 0), (b + 1)| 0 + (w + 1)| 1 + w b+w • w+1 b+w+1 (1, 1), b| 0 + (w + 2)| 1
Reordering the results does not change the statistics, because b • w = w • b. On the other hand, the deterministic alternating coalgebra alt : 2 → 2 × 2 from ( 13) is not exchangeable, since:

(id × alt)(alt(0)) = | ((0, 1), 0)

(swap × 2)((id × alt)(alt(0))) = | ((1, 0), 0) .
Before we state and prove our theorem about exchangeable coalgebras, we also consider a different sequence, which keeps track of the order of draws. We define a sequence h K : X → 2 K × X, with h 0 (x) = ((), x) and h

(K+1) (x) = (2 K ⊗ h) = h K (x). Then we define channels h K : X → 2 K by h K (x) := D(π 1 )(h K (x)) (15)
These constructions are related similar to the earlier constructions h K and h K by

h K = X h K • / / 2 K × X acc×X / / M[K](2) × X h K = X h K • / / 2 K acc / / M[K](2) ,
where acc :

2 K → M[K](2)
is the accumulator map from (4). The difference is that the h variants keep track of the order of draws, which will be useful in our arguments about exchangeability, since h is exchangeable (Definition 5) if and only if

h 2 = D(swap × X) • h 2 : X → 2 × 2 × X.
Lemma 6. Let h : X → 2 × X be an exchangeable coalgebra. Then 1. the map h K can be expressed as:

h K (x) = K k=0 K k • h K (x) 1, . . . , 1 k times , 0, . . . , 0 K-k times k| 1 + (K -k)| 0 . ( 16
)
2. the collection of maps (h K ) forms a cone for the chain of draw-and-delete maps DD (6).

Proof. 1. Among b 1 , . . . , b K ∈ 2 there are K k -many possibilities of having kmany ones. By exchangeability of h there is a normal form with all these ones upfront

h K (x) b 1 , . . . , b K = h K (x) 1, . . . , 1 k times , 0, . . . , 0 K-k times 2. Using (7) we get, for any ϕ = (k|1 + (K -k)| 0 ) ∈ M[K](2), DD • • h K+1 (x)(ϕ) = k+1 K+1 • h K+1 (x)(ϕ + | 1 ) + K+1-k K+1 • h K+1 (ϕ + |0 ) (16) = k+1 K+1 • K+1 k+1 • h K+1 (x) 1, . . . , 1 k+1 times , 0, . . . , 0 + K+1-k K+1 • K+1 k • h K+1 (x) 1, . . . , 1 k times , 0, . . . , 0 = K k • h K+1 (x) 1, . . . , 1 k times , 0, . . . , 0, 1 + h K+1 (x) 1, . . . , 1 k times , 0, . . . , 0 = K k • y h K (x) 1, . . . , 1 k times , 0, . . . , 0, y • h 1 (y)(1) + h 1 (y)(0) = K k • y h K (x) 1, . . . , 1 k times , 0, . . . , 0, y • 1 = K k • h K (x) 1, . . . , 1 k times , 0, . . . , 0 (16)
= h K (x)(ϕ).

Since the Pólya's urn coalgebra pol is exchangeable, the lemma provides another way to deduce that the channels pol K : M * (2) → M[K](2) form a cone [START_REF] Jacobs | Structured probabilistic reasoning[END_REF].

Background on continuous probability

De Finetti's theorem is about the passage from discrete probability to continuous probability. Consider the uniform distribution µ on [0, 1]. The probability of any particular point is 0. So rather than give a probability to individual points, we give probabilities to sets; for example, the probability of a point in the half interval [0, 1 2 ] is 1 2 . In general, a σ-algebra on a set X is a collection of sets Σ that is closed under countable unions and complements. A measurable space (X, Σ) is a set together with a σ-algebra; the sets in Σ are called measurable. In this paper we mainly consider two kinds of σ-algebra, and so they will often be left implicit:

on a countable set (e.g. 2, M(2), M[K](2)) we consider the σ-algebra where every set is measurable. on the unit interval [0, 1], the Borel σ-algebra, which is the least σ-algebra containing the intervals.

On a measurable space (X, Σ), a probability measure is a function ω : Σ → [0, 1] with ω(X) = 1 and with ω( i U i ) = i ω(U i ) when the measurable subsets U i ∈ Σ are pairwise disjoint. On a finite set X the probability measures coincide with the discrete distributions.

The morphisms of measurable spaces are the functions f : X → Y for which the inverse image of a measurable set is measurable. Crucially, if f : X → [0, 1] is measurable and ω : Σ → [0, 1] is a probability measure, then we can find the Lebesgue integral f (x) ω(dx), which is the expected value of f . When X is finite, the Lebesgue integral is a sum: f (x) ω(dx) = X f (x)ω({x}). When X = [0, 1] and ω is the uniform distribution, then the Lebesgue integral is the familiar one.

We write G(X, Σ) for the set of all probability measures on (X, Σ), where we often omit the σ-algebra Σ when it is clear from the context.: D(X) ∼ = G(X), when all subsets are seen as measurable. The set G(X, Σ) itself has a σ-algebra, which is the least σ-algebra making the sets {ω | ω(U ) < r} measurable for all fixed U and r.

Like D, the construction G is a monad, commonly called the Giry monad, but G is a monad on the category of measurable spaces. Maps in the associated Kleisli category K (G) will also be called channels. Thus f : X → Y between measurable spaces can be described as a function f :

X × Σ Y → [0, 1] that is a measure in Σ Y and measurable in X. For a measure ω ∈ G(X) and a channel g : Y → Z we define a new distribution f = ω ∈ G(Y ) and a new channel g • • f : X → Z by Kleisli composition: (f = ω)(U ) := X f (x)(U ) ω(dx) g • • f (x) := g = f (x).
Notice that a discrete channel is in particular a continuous channel, according to our terminology, and so we have an inclusion of Kleisli categories categories K (D) → K (G).

Illustrations from the beta-bernoulli distributions. At the end of Section 4.1, we briefly mentioned the beta-bernoulli distribution as it arises from the coalgebra for Pólya's urn. In general, this beta-binomial channel is defined for arbitrary α, β ∈ R >0 as:

betabin[K](α, β) := 0≤k≤K K k • B(α + k, β + K -k) B(α, β) k|0 +(K -k)| 1 , ( 17
)
This description involves the function B : R >0 × R >0 → R defined as:

B(α, β) := 1 0 x α-1 • (1 -x) β-1 dx ( 18
)
This B is a well-known mathematical function satisfying for instance:

B(α + 1, β) = α α + β • B(α, β) B(n + 1, m + 1) = n! • m! (n + m + 1)! , (19)
for n, m ∈ N. The latter equation shows that ( 11) is an instance of [START_REF] Ścibior | Denotational validation of higher-order Bayesian inference[END_REF].

The function B is also used to define the Beta distribution on the unit interval 1]. We describe it here as a channel in the Kleisli category of the Giry monad:

R >0 × R >0 beta / / G([0, 1]).
It is defined on α, β ∈ R >0 and measurable M ⊆ [0, 1] as:

beta(α, β)(M ) := M x α-1 • (1 -x) β-1 B(α, β) dx. ( 20
)
We prove some basic properties of the beta-binomial channel. These properties are well-known, but are formulated here in slightly non-standard form, using channels.

Lemma 7. 1. A betabinomial channel can itself be decomposed as:

M[K](2) R >0 × R >0 betabin[K] • 6 6 beta • / / [0, 1] binom[K] • O O 2. The beta-binomial channels R >0 × R >0 betabin[K] • / / M[K](2)
for K ∈ N, form a cone for the infinite chain of draw-and-delete channels (6).

Proof. 1. Composition in the Kleisli category K (G) of the Giry monad G yields:

binom[K] • • beta (α, β) k| 0 +(K -k)| 1 = 1 0 K k • x k • (1 -x) K-k • x α-1 • (1 -x) β-1 B(α, β) dx = K k • 1 0 x α+k-1 • (1 -x) β+(K-k)-1 dx B(α, β) (18) = K k • B(α + k, β + K -k) B(α, β) (17) = betabin[K](α, β) k| 0 +(K -k)| 1 .
2. The easiest way to see this is by observing that the channels factorise via the binomial channels binom

[K] : [0, 1] → M[K](2).
In Proposition 2 we have seen that these binomial channels commute with draw-and-delete channels DD.

De Finetti as a limit theorem

We first describe our 'limit' reformulation of the de Finetti theorem and later on argue why this is a reformulation of the original result.

Theorem 8. For X = 2 the cone (8) is a limit in the Kleisli category K (G) of the Giry monad; this limit is the unit interval

[0, 1] ∼ = D(2).
This means that if we have channels

c K : Y → M[K](2) ∼ = {0, 1, . . . , K} with DD • • c K+1 = c K , then there is a unique mediating channel c : Y → [0, 1] with binom[K] • • c = c K , for each K ∈ N.
In the previous section we have seen Below we give the proof, in the current setting. We first illustrate the central role of the draw-and-delete maps DD : M[K + 1](X) → M[K](X) and how they give rise to hypergeometric and binomial distributions.

Via the basic isomorphism M[K](2) ∼ = {0, 1, . . . , K} the draw-and-delete map [START_REF] Fritz | A synthetic approach to Markov kernels, conditional independence, and theorems on sufficient statistics[END_REF] becomes a map DD : {0, . . . , K + 1} → {0, . . . , K}, given by:

DD( ) = K+1 | -1 + K+1- K+1 | . ( 21
)
Notice that the border cases = 0 and = K + 1 are handled implicitly, since the corresponding probabilities are then zero. We can iterate DD, say N times, giving DD N : {0, . . . , K +N } → {0, . . . , K}. If we draw-and-delete N times from an urn with K + N balls, the result is the same as sampling without replacement K times from the same urn. Sampling without replacement is modelled by the hypergeometric distribution. So we can calculate DD N explicitly, using the hypergeometric distribution formula:

DD N ( ) = 0≤k≤K k • K+N - K-k K+N K k .
Implicitly the formal sum is over k ≤ , since otherwise the corresponding probabilities are zero.

As is well known, for large N , the hypergeometric distribution can be approximated by the binomial distribution. To be precise, for fixed K, if ( /K+N) → p as N → ∞, then the hypergeometric distribution DD N ( ) approaches the binomial distribution binom[K](p) as N goes to infinity. This works as follows. Using the notation (n

) m = i<m (n -i) = n(n -1)(n -2) • • • (n -m + 1) we can write n m = (n)m /n! and thus: k • K+N - K-k K+N K = ( ) k k! • (K + N -) K-k (K -k)! • K! (K + N ) K = K k • ( ) k • (K + N -) K-k (K + N ) K = K k • i<k ( -i) • i<K-k (K + N --i) i<K (K + N -i) = K k • i<k ( /K+N -i /K+N) • i<K-k (1 -/K+N -i /K+N) i<K (1 -i /K+N) → K k • p k • (1 -p) K-k as N → ∞ = binom[K](p)(k).
The proof of Theorem 8 makes use of a classical result of Hausdorff [START_REF] Hausdorff | Summationsmethoden und Momentfolgen I[END_REF], giving a criterion for the existence of probability measures. It is repeated here without proof (but see e.g. [START_REF] Feller | An Introduction to Probability Theory and Its applications[END_REF] for details).

Recall that the moments of a distribution µ ∈ G([0, 1]) form a sequence of numbers m 1 , . . . , m K , . . . ∈ [0, 1] given by m K = 1 0 r K µ(dr): the expected values of r K . In general, moments correspond to statistical concepts such as mean, variance, skew and so on. But in this specific case, the K-th moment of µ is the probability (binom[K] = µ)(K) that K balls drawn will all be black.

Recall that a sequence a = (a n ) is completely monotone if:

(-1) k • ∆ k a n ≥ 0 for all n, k.
This formulation involves the difference operator ∆ on sequences, given by (∆a) n = a n+1 -a n . This operator is iterated, in the standard way as ∆ 0 = id and

∆ m+1 = ∆ • ∆ m .
Theorem 9 (Hausdorff ). A sequence a = (a n ) n∈N of non-negative real numbers a n is completely monotone if and only if it arises as sequence of moments: there is a unique measure µ ∈ G([0, 1]) with, for each n,

a n = 1 0
x n µ(dx).

Proof (of Theorem 8). As a first step, we shall reason pointwise. Let, for each K ∈ N, a distribution ω K ∈ D({0, 1, . . . , K}) be given, with DD = ω K+1 = ω K .

We need to produce a unique (continuous

) distribution ω ∈ G([0, 1]) such that ω K = binom[K] = ω, for each K.
The problem of finding ω is essentially Hausdorff's moment problem, see Theorem 9. The connection between Hausdorff's moments problem and de Finetti's theorem is well known [6, §VII.4], but the connection is particularly apparent in our channel-based formulation.

We exploit Hausdorff's criterion via two claims, which we elaborate in some detail. The first one is standard.

Claim 1. If µ ∈ G([0, 1]) has moments m K , then: 1 0 x n • (1 -x) k µ(dx) = (-1) k • ∆ k m n .
This equation can be proven by induction on k. It holds by definition of m for k = 0. Next:

1 0 x n • (1 -x) k+1 µ(dx) = 1 0 x n • (1 -x) • (1 -x) k µ(dx) = 1 0 x n • (1 -x) k µ(dx) - 1 0 x n+1 • (1 -x) k µ(dx) (IH) = (-1) k • ∆ k m n -(-1) k • ∆ k m n+1 = (-1) k+1 • ∆ k m n+1 -∆ k m n = (-1) k+1 • ∆ k+1 m n .
The next claim involves a crucial observation about our setting: the whole sequence of distributions ω K ∈ D({0, 1, . . . , K}) is entirely determined by the probabilities ω K (K) of drawing K balls which are all black.

Claim 2. The numbers b K := ω K (K) ∈ [0, 1], for K ∈ N, determine all the distributions ω K via the relationship:

ω k+n (n) = k+n n • (-1) k • ∆ k b n .
In particular, the sequence b K is completely monotone.

The proof works again by induction on k. The case k = 0 holds by definition. For the induction step we use the cone property DD = ω k+1 = ω k . Via (21) it gives:

ω k (i) = i+1 k+1 • ω k+1 (i + 1) + k+1-i k+1 • ω k+1 (i),
so that:

ω k+1 (i) = k+1 k+1-i • ω k (i) -i+1 k+1-i • ω k+1 (i + 1).
We use this equation in the first step below.

ω (k+1)+n (n) = k+1+n k+1 • ω k+n (n) -n+1 k+1 • ω k+1+n (n + 1) (IH) = k+1+n k+1 • k+n n • (-1) k • ∆ k b n -n+1 k+1 • k+1+n n+1 • (-1) k • ∆ k b n+1 = k+1+n n • (-1) k+1 • ∆ k b n+1 -∆ k b n = k+1+n n • (-1) k+1 • ∆ k+1 b n .
This second claim implies that there is a unique distribution ω ∈ G([0, 1]) whose K-th moments equals b K = ω K (K). But then:

ω K (k) = ω (K-k)+k (k) = K k • (-1) K-k • ∆ K-k b k by Claim 2 = K k • 1 0 x k • (1 -x) K-k dω(x) by Claim 1 = binom[K] = ω (k).
As an aside, it is perhaps instructive to look at how the distribution ω ∈ G([0, 1]) is built in the proof of Hausdorff's criterion. One way is as a limiting measure of the sequence of finite discrete distributions on [0, 1],

ω K := K k=0 ω K (k) k K . (22)
This is illustrated in the following table , for the examples of the binomial cone and the uniform cone. The graphs show ωK (plotted as densities with respect to the counting measure). We conclude by explaining why this construction gives a measurable mediating map. Suppose we have a measurable space (Y, Σ) and a sequence of channels c K : Y → {0, . . . , K} forming a cone over [START_REF] Fritz | The zero-one laws of Kolmogorov and Hewitt-Savage in categorical probability[END_REF], i.e. c K = DD • • c K+1 for all K ∈ N. We define a mediating channel c : Y → [0, 1] by putting the distribution c(y) as the unique one with moments c K (y)(K), as above. It remains to show that c, regarded as a function Y → G([0, 1]), is a measurable function. It is immediate that the sequence-of-moments function m : Y → [0, 1] ∞ given by: m(y) K :=

K = 5 K = 10 K = 50 limit(K → ∞) ωK = binom[K](0.
1 0 r K c(x)(dr) = c K (y)(K).
is measurable, because the c K 's are assumed to be channels: let V ⊆ [0, 1] be measurable; for associated basic measurable subsets of [0, 1] ∞ one has:

m -1 [0, 1] K × V × [0, 1] ∞ = {y ∈ Y | c K (y)(K) ∈ V } = c -1 K [0, 1] K × V . Further, c : Y → G([0, 1]) factors through m; indeed G([0, 1]
) can be thought of as a subset of [0, 1] ∞ , when each distribution is regarded as its sequence of moments. We conclude by the less well-known fact that

G([0, 1]) is a subspace of [0, 1] ∞ .
Theorem 8 is a reformulation of a classical result of de Finetti [START_REF] De Finetti | Funzione caratteristica di un fenomeno aleatorio[END_REF]. It introduced the concept of exchangeability of random variables which has disappeared completely from our reformulation, but is implicit in our use of multisets. This requires some explanation.

A (discrete) random variable is a pair ρ ∈ D(A), U : A → R of a distribution and an observable. Usually the distribution ρ is implicit. Instead, the notation P (U ) is used for the image distribution D(U )(ρ) on R, also sometimes written as P (U = r), for r ∈ R.

Let (U 1 , ρ 1 ), . . . , (U n , ρ n ) be a finite sequence of random variables. It induces a joint distribution on R n ,

P (U 1 , . . . , U n ) := D U 1 × • • • × U n ρ 1 ⊗ • • • ⊗ ρ n , where U 1 × • • • × U n : A 1 × • • • × A n → R n and ρ 1 ⊗ • • • ⊗ ρ n ∈ D(A 1 × • • • × A n ).
Such a sequence (U i , ρ i ) is called exchangeable if for each permutation π:

P (U 1 , . . . , U n ) = P (U π(1) , . . . , U π(n) ).
An infinite sequence is called exchangeable if each finite subsequence is exchangeable.

The original form of de Finetti's theorem involves binary (0-1) random variables with U i : A i → 2 = {0, 1} → R. The distribution P (U i ) is then on a 'Bernouilli' distribution on 2. When random variables are exchangeable their order doesn't matter but only how many of them are zero or one. This is captured by their sum i U i . But this sum is a multiset over 2. Indeed, in a multset, the order of elements does not matter, only their multiplicities (numbers of occurrences). This is a crucial observation underlying our reformulation, that already applied to the accumulator map acc in (4). But let's first look at the usual formulation of de Finetti's (binary) representation theorem, see [START_REF] De Finetti | Funzione caratteristica di un fenomeno aleatorio[END_REF] and the textbooks [START_REF] Feller | An Introduction to Probability Theory and Its applications[END_REF][START_REF] Klenke | Probability Theory[END_REF].

Theorem 10. Let U 1 , U 2 , . . . be an infinite sequence of exchangeable binary random variables. Then there is a probability measure ω on [0, 1] such that for all n,

P (U 1 , . . . , U n ) = 1 0 x i Ui (1 -x) (n-i Ui) ω( dx).
It is clear that there is a considerable gap between this original formulation and the inverse limit formulation that has been developed in this paper. There is room for narrowing this gap.

The essence that is used in de Finetti's theorem about n exchangeable binary random variables are their outcomes via the accumulator map acc from (4), giving a map D(acc) :

D(2 n ) → D(M[n](2)).
In our approach we have reformulated the requirements about random variables and about exchangeability and worked directly with distributions on multisets, see Proposition 2 and Theorem 8. De Finetti's (binary) representation Theorem 10 becomes a limit statement in a Kleisli category. We think that this approach brings forward the mathematical essentials.

A final exchangeable coalgebra

We return to the setting of coalgebras, begun in Section 4. Any coalgebra h : X → 2 × X for the functor 2 × (-) on K (D) or on K (G) is a probabilistic process that produces a random infinite sequence of boolean values. Following [START_REF] Kerstan | Coalgebraic trace semantics for probabilistic transition systems based on measure theory[END_REF], we can understand this induced sequence as arising from the fact that the pair of head and tail function 2

∞ ∼ = / / 2 × 2 ∞
is a final coalgebra in the category K (G), and so there is a unique channel h : X → 2 ∞ assigning to each element of X the random sequence that it generates. Here 2 ∞ is the measurable space of infinite binary streams, regarded with the product σ-algebra.

It is helpful to spell this construction out a little. The sequence of first projections

2 0 2 1 o o 2 2 o o 2 3 o o • • • o o (23)
has as a limit the space 2 ∞ , with the limiting cone being the obvious projections. And this limit is also a limit in K (G). (This is a categorical formulation of Kolmogorov's extension theorem, see [4, Thm. 2.5].) Now, as usual in coalgebra theory, we find h : X → 2 ∞ for any coalgebra h : X → 2 × X by noticing that the channels h K : X → 2 K (15) define a cone over the chain (23). The limiting channel h : X → 2 ∞ for the cone is the unique coalgebra homomorphism to the final coalgebra.

Example 11. We define the bernoulli coalgebra to be the channel bern : [0, 1] → 2 × [0, 1] given by bern(r) := r • |1, r + (1 -r) • | 0, r . In words, bern(r) makes a coin toss with known bias r and returns the outcome together with the same bias r unchanged.

The final channel iid := bern : [0, 1] → 2 ∞ takes a probability r to a random infinite sequence of independent and identically distributed binary values, all distributed as r| 1 + (1 -r)| 0 . More explicitly, for basic measurable subsets, at each stage n,

iid(r) 2 n × {1} × 2 ∞ = r and iid(r) 2 n × {0} × 2 ∞ = 1 -r.
So, any coalgebra defines a cone over (23). We have shown in Lemma 6 that any exchangeable coalgebra defines a cone over the draw-delete chain [START_REF] Feller | An Introduction to Probability Theory and Its applications[END_REF]. We use this to show that the bernoulli coalgebra bern :

[0, 1] → 2 × [0, 1] is the final exchangeable coalgebra.
The final coalgebra 2 ∞ → 2 × 2 ∞ is not exchangeable. To see this, consider the infinite alternating sequence 01010101 • • • ∈ 2 ∞ , so that the left hand side of ( 14) at the sequence gives (0, 1, 010101 . . . ), whereas the right hand side of ( 14) at the sequence gives (1, 0, 010101 . . . ), which is different.

The bernoulli coalgebra bern : [0, 1] → 2 × [0, 1] is exchangeable, because (id ⊗ bern) = bern(r) = r 2 1, 1, r +

(1 -r)r 0, 1, r + r(1 -r)| 1, 0, r + (1 -r) 2 0, 0, r .

Notice that reordering the outputs does not change the statistics.

Theorem 12. The bernoulli coalgebra bern : [0, 1] → 2 × [0, 1] is the final exchangeable coalgebra.

Proof. Let h : X → 2 × X be an exchangeable coalgebra. By Lemma 6 the associated maps h K : X → M[K](2) form a cone. By de Finetti's theorem in limit form -that is, by Theorem 8 -we get a unique mediating channel f : X → [0, 1] with binom[K] • • f = h K for each K. Our aim is to show that f is a unique coalgebra map: bern

• • f = (id ⊗ f ) • • h.
We do know that the limiting map X • f / / [0, 1] • iid / / 2 ∞ is a unique coalgebra homomorphism. So to show that f is a unique coalgebra homomorphism, it suffices to show that iid is a monomorphism in K (G).

To see this, first notice that the K-th moment of some distribution ω ∈ G([0, 1]) is the probability (iid = ω)({1} K ×2 ∞ ), and so if two random sequences are equal, iid = ω 1 = iid = ω 2 , then in particular the moments of ω 1 and ω 2 are equal and so ω 1 = ω 2 . Moreover the endofunctor 2×-preserves monomorphisms. So if the final channel X → 2 ∞ factors through iid : [0, 1] → 2 ∞ as a channel then it also factors through as a coalgebra homomorphism, necessarily uniquely, by the definition of monomorphism.

Example 13. We return to the example of Pólya's urn coalgebra pol : M * (2) → 2 × M * (2). We have shown in Proposition 4 that the cone pol K : M * (2) → M[K](2) defined by iterated draws is given by the beta-bernoulli distributions: pol K (ϕ) = betabern[K](ϕ(0), ϕ(1)), and we have shown in Proposition 7 that the beta-bernoulli cone over (6) has mediating map the beta distribution. So the final channel beta : M * (2) → [0, 1] is given by putting beta(ϕ) as the beta distribution with parameters (ϕ(0), ϕ(1)), and this is a coalgebra homomorphism. The commuting diagram M * (2)

• beta

• pol / / 2 × M * (2) • 2×beta [0, 1] • bern / / 2 × [0, 1]
expresses the 'conjugacy' between the bernoulli and beta distributions, see also [START_REF] Jacobs | A channel-based perspective on conjugate priors[END_REF].

Conclusions and further work

This paper has translated the classical representation theorem of de Finetti into the language of multisets and distributions and turned it into a limit theorem. This limit is subsequently used for a finality result for exchangeable coalgebras.

We have concentrated, as is usual for the de Finetti theorem, on the binary case, giving a limit statement for the special case X = 2 = {0, 1} of the cone in Proposition 2. There is an obvious question whether this formulation can be extended to X = {0, 1, . . . , n -1} for n > 2, or to more general measurable spaces. We see two possible avenues:

extension to finite sets via a multivariate version of Hausdorff's moments theorem, see [START_REF] Kleiber | Multivariate distributions and the moment problem[END_REF]; extension to Polish spaces, following [START_REF] Dahlqvist | Robustly parameterised higher-order probabilistic models[END_REF] and its categorical justification for extending de Finetti's theorem to such spaces (esp. Theorems 35 and 40) in terms of exchangeability.

Another point for future work is to investigate whether the categorical formulation of de Finetti's theorem could be taken as an axiom for a 'synthetic probability theory' (e.g. following [START_REF] Fritz | A synthetic approach to Markov kernels, conditional independence, and theorems on sufficient statistics[END_REF][START_REF] Fritz | The zero-one laws of Kolmogorov and Hewitt-Savage in categorical probability[END_REF][START_REF] Ścibior | Denotational validation of higher-order Bayesian inference[END_REF]), and indeed whether it holds in some proposed categorical models which do support de-Finetti-like arguments ( [START_REF] Heunen | A convenient category for higherorder probability theory[END_REF][START_REF] Staton | The Beta-Bernoulli process and algebraic effects[END_REF]). Finally, we note that chains of channels between multisets also arise in recent exponential modalities for linear logic [START_REF] Dahlqvist | Semantics of higher-order probabilistic programs with conditioning[END_REF][START_REF] Hamano | A linear exponential comonad in s-finite transition kernels and probabilistic coherent spaces[END_REF]; the connections remain to be worked out.

  n (1 -r) k-n dr = 1 k+1

  an example with Y = R >0 × R >0 and c K = betabin[K] : Y → M[K](2) and mediating channel c = beta : Y → [0, 1].

Acknowledgements. Staton is supported by a Royal Society Fellowship, and has enjoyed discussions about formulations of de Finetti's theorem with many people including coauthors on [18].