The category of complete atomic boolean algebras $\mathbf{CABA}$ is equivalent to $\mathbf{Set}^{\mathrm{op}}$ via $$\mathbf{Set}^{\mathrm{op}} \to \mathbf{CABA}, ~ X \mapsto (P(X),\bigcup,\bigcap).$$ The inverse takes the atoms. The functor $P : \mathbf{Set}^{\mathrm{op}} \to \mathbf{Set}$ is monadic, its left adjoint is $P^{\mathrm{op}}$. From this we deduce that $\mathbf{CABA}$ is monadic over $\mathbf{Set}$, and that the free CABA on a set $X$ is $(P(P(X)),\bigcup,\bigcap)$ with the inclusion $$\mathrm{prin} : X \to P(P(X)),~ x \mapsto \{A : x \in A\}.$$ One can also work out the following formula which expresses every element $S \in P(P(X))$ in terms of the generators: $$S = \bigvee_{A \in S} \left(\bigwedge_{x \in A} \mathrm{prin}(x) \wedge \bigwedge_{x \notin A} \neg \mathrm{prin}(x)\right)$$ Anyway, since $\mathbf{CABA}$ is monadic over $\mathbf{Set}$, we can define$^{(1)}$ for any complete category $\mathcal{C}$ (powers are sufficient, actually) the category of internal CABAs $\mathbf{CABA}(\mathcal{C})$.

Question. What is an intuitive way of thinking about internal CABA structures on an object $B \in \mathcal{C}$? More specifically, is there any description which (A) makes the forgetful functor $$\mathbf{CABA}(\mathcal{C}) \to \mathbf{CBA}(\mathcal{C})$$ to complete boolean algebras explicit (I hope that there is no problem with the non-existence of free CBAs), and (B) describes the image of this functor, i.e. saying what "being atomic" actually means for an internal complete boolean algebra?

Currently I only know the following descriptions, which do not answer the question so far.

1. We have $\mathbf{CABA}(\mathcal{C}) \simeq \mathrm{Hom}_{\mathrm{cont.}}(\mathbf{Set},\mathcal{C})$. An internal CABA structure on $B$ is a continuous functor $F : \mathbf{Set} \to \mathcal{C}$ with $F(2)=B$. This is very abstract, though.

2. An internal CABA structure on $B$ consists of natural maps $P(P(X)) \to \hom(B^X,B)$ which satisfy two axioms (more concisely, monad maps from $P \circ P^{\mathrm{op}} $ to the double dualization monad of $B$.) The unit axiom is just that $\mathrm{prin}(x)$ gets mapped to the projection $p_x$, but the other axiom looks awful. Is there any way we can simplify this? And how are the union, intersection and complement operators on $B$ derived from this?

Any references to the literature dealing with $\mathbf{CABA}(\mathcal{C})$ are appreciated as well.

$^{(1)}$If $T$ is a monad on $\mathbf{Set}$, a $T$-algebra structure on $B \in \mathbf{Set}$ can be described with a monad map $ T(X) \to \hom(B^X,B)$. This description can therefore be generalized to objects $B \in \mathcal{C}$ of a category $\mathcal{C}$ with powers. So we actually can define $ \mathrm{Alg}_{\mathcal{C}}(T)$, not just $\mathrm{Alg}(T)$. This can also be seen via the equivalence between monads and infinitary Lawvere theories.

The category of complete atomic boolean algebras $\mathbf{CABA}$ is equivalent to $\mathbf{Set}^{\mathrm{op}}$ via $$\mathbf{Set}^{\mathrm{op}} \to \mathbf{CABA}, ~ X \mapsto (P(X),\bigcup,\bigcap).$$ The inverse takes the atoms. The functor $P : \mathbf{Set}^{\mathrm{op}} \to \mathbf{Set}$ is monadic, its left adjoint is $P^{\mathrm{op}}$. From this we deduce that $\mathbf{CABA}$ is monadic over $\mathbf{Set}$, and that the free CABA on a set $X$ is $(P(P(X)),\bigcup,\bigcap)$ with the inclusion $$\mathrm{prin} : X \to P(P(X)),~ x \mapsto \{A : x \in A\}.$$ One can also work out the following formula which expresses every element $S \in P(P(X))$ in terms of the generators: $$S = \bigvee_{A \in S} \left(\bigwedge_{x \in A} \mathrm{prin}(x) \wedge \bigwedge_{x \notin A} \neg \mathrm{prin}(x)\right)$$ Anyway, since $\mathbf{CABA}$ is monadic over $\mathbf{Set}$, we can define$^{(1)}$ for any complete category $\mathcal{C}$ (powers are sufficient, actually) the category of internal CABAs $\mathbf{CABA}(\mathcal{C})$.

Question. What is an intuitive way of thinking about internal CABA structures on an object $B \in \mathcal{C}$? More specifically, is there any description which (A) makes the forgetful functor $$\mathbf{CABA}(\mathcal{C}) \to \mathbf{CBA}(\mathcal{C})$$ to complete boolean algebras explicit (I hope that there is no problem with the non-existence of free CBAs), and (B) describes the image of this functor, i.e. saying what "being atomic" actually means for an internal complete boolean algebra?

Currently I only know the following descriptions, which do not answer the question so far.

1. We have $\mathbf{CABA}(\mathcal{C}) \simeq \mathrm{Hom}_{\mathrm{cont.}}(\mathbf{Set},\mathcal{C})$. An internal CABA structure on $B$ is a continuous functor $F : \mathbf{Set} \to \mathcal{C}$ with $F(2)=B$. This is very abstract, though.

2. An internal CABA structure on $B$ consists of natural maps $P(P(X)) \to \hom(B^X,B)$ which satisfy two axioms (more concisely, monad maps from $P \circ P^{\mathrm{op}} $ to the double dualization monad of $B$.) The unit axiom is just that $\mathrm{prin}(x)$ gets mapped to the projection $p_x$, but the other axiom looks awful. Is there any way we can simplify this? And how are the union, intersection and complement operators on $B$ derived from this?

Any references to the literature dealing with $\mathbf{CABA}(\mathcal{C})$ are appreciated as well.

$^{(1)}$If $T$ is a monad on $\mathbf{Set}$, a $T$-algebra structure on $B \in \mathbf{Set}$ can be described with a monad map $ T(X) \to \hom(B^X,B)$. This description can therefore be generalized to objects $B \in \mathcal{C}$ of a category $\mathcal{C}$ with powers. So we actually can define $ \mathrm{Alg}_{\mathcal{C}}(T)$, not just $\mathrm{Alg}(T)$. This can also be seen via the equivalence between monads and infinitary Lawvere theories.

Edit. Here is an idea: The universal property of $P(P(X))$ above implies that for every CABA $B$ and every map $f : X \to B$ the map $\tilde{f} : P(P(X)) \to B$ defined by

$$\tilde{f}(S) := \bigvee_{A \in S} \left(\bigwedge_{x \in A} f(x) \wedge \bigwedge_{x \notin A} \neg f(x)\right)$$

is a homomorphism of boolean algebras. It is clearly compatible with joins, so the statement reduces to the compatibility of complements. That is, for all $S \in P(P(X))$ $$\bigvee_{A \notin S} \left(\bigwedge_{x \in A} f(x) \wedge \bigwedge_{x \notin A} \neg f(x)\right) = \bigwedge_{A \in S} \left(\bigvee_{x \in A} \neg f(x) \vee \bigvee_{x \notin A} f(x)\right)$$ This equation can be written down for internal complete boolean algebras as well (replace $f$ by a generalized element of $B^X$), and it seems to be a necessary condition for being atomic.

The category of complete atomic boolean algebras $\mathbf{CABA}$ is equivalent to $\mathbf{Set}^{\mathrm{op}}$ via $$\mathbf{Set}^{\mathrm{op}} \to \mathbf{CABA}, ~ X \mapsto (P(X),\bigcup,\bigcap).$$ The inverse takes the atoms. The functor $P : \mathbf{Set}^{\mathrm{op}} \to \mathbf{Set}$ is monadic, its left adjoint is $P^{\mathrm{op}}$. From this we deduce that $\mathbf{CABA}$ is monadic over $\mathbf{Set}$, and that the free CABA on a set $X$ is $(P(P(X)),\bigcup,\bigcap)$ with the inclusion $$\mathrm{prin} : X \to P(P(X)),~ x \mapsto \{A : x \in A\}.$$ One can also work out the following formula which expresses every element $S \in P(P(X))$ in terms of the generators: $$S = \bigvee_{A \in S} \left(\bigwedge_{x \in A} \mathrm{prin}(x) \wedge \bigwedge_{x \notin A} \neg \mathrm{prin}(x)\right)$$ Anyway, since $\mathbf{CABA}$ is monadic over $\mathbf{Set}$, we can define for any complete category $\mathcal{C}$ (products are sufficient, actually) the category of internal CABAs $\mathbf{CABA}(\mathcal{C})$.

Question. What is an intuitive way of thinking about internal CABA structures on an object $B \in \mathcal{C}$? More specifically, is there any description which (A) makes the forgetful functor $$\mathbf{CABA}(\mathcal{C}) \to \mathbf{CBA}(\mathcal{C})$$ to complete boolean algebras explicit (I hope that there is no problem with the non-existence of free CBAs), and (B) describes the image of this functor, i.e. saying what "being atomic" actually means for an internal complete boolean algebra?

Currently I only know the following descriptions, which do not answer the question so far.

1. We have $\mathbf{CABA}(\mathcal{C}) \simeq \mathrm{Hom}_{\mathrm{cont.}}(\mathbf{Set},\mathcal{C})$. An internal CABA structure on $B$ is a continuous functor $F : \mathbf{Set} \to \mathcal{C}$ with $F(2)=B$. This is very abstract, though.

2. An internal CABA structure on $B$ consists of maps $P(P(X)) \to \hom(B^X,B)$ which satisfy two axioms (more concisely, monad maps from $P \circ P^{\mathrm{op}} $ to the double dualization monad of $B$.) The unit axiom is just that $\mathrm{prin}(x)$ gets mapped to the projection $p_x$, but the other axiom looks awful. Is there any way we can simplify this?

Any references to the literature dealing with $\mathbf{CABA}(\mathcal{C})$ are appreciated as well.

The category of complete atomic boolean algebras $\mathbf{CABA}$ is equivalent to $\mathbf{Set}^{\mathrm{op}}$ via $$\mathbf{Set}^{\mathrm{op}} \to \mathbf{CABA}, ~ X \mapsto (P(X),\bigcup,\bigcap).$$ The inverse takes the atoms. The functor $P : \mathbf{Set}^{\mathrm{op}} \to \mathbf{Set}$ is monadic, its left adjoint is $P^{\mathrm{op}}$. From this we deduce that $\mathbf{CABA}$ is monadic over $\mathbf{Set}$, and that the free CABA on a set $X$ is $(P(P(X)),\bigcup,\bigcap)$ with the inclusion $$\mathrm{prin} : X \to P(P(X)),~ x \mapsto \{A : x \in A\}.$$ One can also work out the following formula which expresses every element $S \in P(P(X))$ in terms of the generators: $$S = \bigvee_{A \in S} \left(\bigwedge_{x \in A} \mathrm{prin}(x) \wedge \bigwedge_{x \notin A} \neg \mathrm{prin}(x)\right)$$ Anyway, since $\mathbf{CABA}$ is monadic over $\mathbf{Set}$, we can define$^{(1)}$ for any complete category $\mathcal{C}$ (powers are sufficient, actually) the category of internal CABAs $\mathbf{CABA}(\mathcal{C})$.

Question. What is an intuitive way of thinking about internal CABA structures on an object $B \in \mathcal{C}$? More specifically, is there any description which (A) makes the forgetful functor $$\mathbf{CABA}(\mathcal{C}) \to \mathbf{CBA}(\mathcal{C})$$ to complete boolean algebras explicit (I hope that there is no problem with the non-existence of free CBAs), and (B) describes the image of this functor, i.e. saying what "being atomic" actually means for an internal complete boolean algebra?

Currently I only know the following descriptions, which do not answer the question so far.

1. We have $\mathbf{CABA}(\mathcal{C}) \simeq \mathrm{Hom}_{\mathrm{cont.}}(\mathbf{Set},\mathcal{C})$. An internal CABA structure on $B$ is a continuous functor $F : \mathbf{Set} \to \mathcal{C}$ with $F(2)=B$. This is very abstract, though.

2. An internal CABA structure on $B$ consists of natural maps $P(P(X)) \to \hom(B^X,B)$ which satisfy two axioms (more concisely, monad maps from $P \circ P^{\mathrm{op}} $ to the double dualization monad of $B$.) The unit axiom is just that $\mathrm{prin}(x)$ gets mapped to the projection $p_x$, but the other axiom looks awful. Is there any way we can simplify this? And how are the union, intersection and complement operators on $B$ derived from this?

Any references to the literature dealing with $\mathbf{CABA}(\mathcal{C})$ are appreciated as well.

$^{(1)}$If $T$ is a monad on $\mathbf{Set}$, a $T$-algebra structure on $B \in \mathbf{Set}$ can be described with a monad map $ T(X) \to \hom(B^X,B)$. This description can therefore be generalized to objects $B \in \mathcal{C}$ of a category $\mathcal{C}$ with powers. So we actually can define $ \mathrm{Alg}_{\mathcal{C}}(T)$, not just $\mathrm{Alg}(T)$. This can also be seen via the equivalence between monads and infinitary Lawvere theories.