The Clowder Project

Let $X$ be a set.

1. Co/Completeness. The (posetal) category (associated to) $\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright )$ is complete and cocomplete:
   1. Products. The products in $\mathcal{P}\webleft (X\webright )$ are given by intersection of subsets.
   2. Coproducts. The coproducts in $\mathcal{P}\webleft (X\webright )$ are given by union of subsets.
   3. Co/Equalisers. Being a posetal category, $\mathcal{P}\webleft (X\webright )$ only has at most one morphisms between any two objects, so co/equalisers are trivial.
2. Cartesian Closedness. The category $\mathcal{P}\webleft (X\webright )$ is Cartesian closed with internal Hom
   \[ \mathbf{Hom}_{\mathcal{P}\webleft (X\webright )}\webleft (-_{1},-_{2}\webright )\colon \mathcal{P}\webleft (X\webright )\mkern -0.0mu^{\mathsf{op}}\times \mathcal{P}\webleft (X\webright ) \to \mathcal{P}\webleft (X\webright ) \]

   given by^[2]

   \[ \mathbf{Hom}_{\mathcal{P}\webleft (X\webright )}\webleft (U,V\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (X\setminus U\webright )\cup V \]

   for each $U,V\in \text{Obj}\webleft (\mathcal{P}\webleft (X\webright )\webright )$.

Let $X$ be a set.

1. Functoriality I. The assignment $X\mapsto \mathcal{P}\webleft (X\webright )$ defines a functor
   \[ \mathcal{P}_{*}\colon \mathsf{Sets}\to \mathsf{Sets}, \]

   where

   • Action on Objects. For each $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, we have
     \[ \mathcal{P}_{*}\webleft (A\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathcal{P}\webleft (A\webright ). \]

   • Action on Morphisms. For each $A,B\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, the action on morphisms
     \[ \mathcal{P}_{*|A,B}\colon \mathsf{Sets}\webleft (A,B\webright )\to \mathsf{Sets}\webleft (\mathcal{P}\webleft (A\webright ),\mathcal{P}\webleft (B\webright )\webright ) \]

     of $\mathcal{P}_{*}$ at $\webleft (A,B\webright )$ is the map defined by by sending a map of sets $f\colon A\to B$ to the map

     \[ \mathcal{P}_{*}\webleft (f\webright )\colon \mathcal{P}\webleft (A\webright )\to \mathcal{P}\webleft (B\webright ) \]

     defined by

     \[ \mathcal{P}_{*}\webleft (f\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f_{*}, \]

     as in Definition 2.4.4.1.1.

2. Functoriality II. The assignment $X\mapsto \mathcal{P}\webleft (X\webright )$ defines a functor
   \[ \mathcal{P}^{-1}\colon \mathsf{Sets}^{\mathsf{op}}\to \mathsf{Sets}, \]

   where

   • Action on Objects. For each $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, we have
     \[ \mathcal{P}^{-1}\webleft (A\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathcal{P}\webleft (A\webright ). \]

   • Action on Morphisms. For each $A,B\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, the action on morphisms
     \[ \mathcal{P}^{-1}_{A,B}\colon \mathsf{Sets}\webleft (A,B\webright )\to \mathsf{Sets}\webleft (\mathcal{P}\webleft (B\webright ),\mathcal{P}\webleft (A\webright )\webright ) \]

     of $\mathcal{P}^{-1}$ at $\webleft (A,B\webright )$ is the map defined by by sending a map of sets $f\colon A\to B$ to the map

     \[ \mathcal{P}^{-1}\webleft (f\webright )\colon \mathcal{P}\webleft (B\webright )\to \mathcal{P}\webleft (A\webright ) \]

     defined by

     \[ \mathcal{P}^{-1}\webleft (f\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f^{-1}, \]

     as in Definition 2.4.5.1.1.

3. Functoriality III. The assignment $X\mapsto \mathcal{P}\webleft (X\webright )$ defines a functor
   \[ \mathcal{P}_{!}\colon \mathsf{Sets}\to \mathsf{Sets}, \]

   where

   • Action on Objects. For each $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, we have
     \[ \mathcal{P}_{!}\webleft (A\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathcal{P}\webleft (A\webright ). \]

   • Action on Morphisms. For each $A,B\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, the action on morphisms
     \[ \mathcal{P}_{!|A,B}\colon \mathsf{Sets}\webleft (A,B\webright )\to \mathsf{Sets}\webleft (\mathcal{P}\webleft (A\webright ),\mathcal{P}\webleft (B\webright )\webright ) \]

     of $\mathcal{P}_{!}$ at $\webleft (A,B\webright )$ is the map defined by by sending a map of sets $f\colon A\to B$ to the map

     \[ \mathcal{P}_{!}\webleft (f\webright )\colon \mathcal{P}\webleft (A\webright )\to \mathcal{P}\webleft (B\webright ) \]

     defined by

     \[ \mathcal{P}_{!}\webleft (f\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f_{!}, \]

     as in Definition 2.4.6.1.1.

4. Adjointness I. We have an adjunction
   
   witnessed by a bijection
   \[ \underbrace{\mathsf{Sets}^{\mathsf{op}}\webleft (\mathcal{P}\webleft (A\webright ),B\webright )}_{\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mkern 5mu\mathsf{Sets}\webleft (B,\mathcal{P}\webleft (A\webright )\webright )} \cong \mathsf{Sets}\webleft (A,\mathcal{P}\webleft (B\webright )\webright ), \]

   natural in $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ and $B\in \text{Obj}\webleft (\mathsf{Sets}^{\mathsf{op}}\webright )$.

5. Adjointness II. We have an adjunction
   
   witnessed by a bijection of sets
   \[ \mathrm{Rel}\webleft (\text{Gr}\webleft (A\webright ),B\webright ) \cong \mathsf{Sets}\webleft (A,\mathcal{P}\webleft (B\webright )\webright ) \]

   natural in $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ and $B\in \text{Obj}\webleft (\mathrm{Rel}\webright )$, where $\text{Gr}$ is the graph functor of Chapter 6: Constructions With Relations, Item 1 of Proposition 6.3.1.1.2 and $\mathcal{P}_{*}$ is the functor of Chapter 6: Constructions With Relations, Proposition 6.4.5.1.1.

Let $X$ be a set.

1. Symmetric Strong Monoidality With Respect to Coproducts I. The powerset functor $\mathcal{P}_{*}$ of Item 1 of Proposition 2.4.3.1.4 has a symmetric strong monoidal structure
   \[ \webleft (\mathcal{P}_{*},\mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{*},\mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{*|\mathbb {1}}\webright ) \colon \webleft (\mathsf{Sets},\times ,\text{pt}\webright ) \to \webleft (\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\emptyset \webright ) \]

   being equipped with isomorphisms

   \[ \begin{gathered} \mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{*|X,Y} \colon \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright ) \xrightarrow {\cong }\mathcal{P}\webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright ),\\ \mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{*|\mathbb {1}} \colon \text{pt}\xrightarrow {\cong }\mathcal{P}\webleft (\emptyset \webright ), \end{gathered} \]

   natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.

2. Symmetric Strong Monoidality With Respect to Coproducts II. The powerset functor $\mathcal{P}^{-1}$ of Item 2 of Proposition 2.4.3.1.4 has a symmetric strong monoidal structure
   \[ \webleft (\mathcal{P}^{-1},\mathcal{P}^{-1|\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}},\mathcal{P}^{-1|\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{\mathbb {1}}\webright ) \colon \webleft (\mathsf{Sets}^{\mathsf{op}},\times ^{\mathsf{op}},\text{pt}\webright ) \to \webleft (\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\emptyset \webright ) \]

   being equipped with isomorphisms

   \[ \begin{gathered} \mathcal{P}^{-1|\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{X,Y} \colon \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright ) \xrightarrow {\cong }\mathcal{P}\webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright ),\\ \mathcal{P}^{-1|\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{\mathbb {1}} \colon \text{pt}\xrightarrow {\cong }\mathcal{P}\webleft (\emptyset \webright ), \end{gathered} \]

   natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.

3. Symmetric Strong Monoidality With Respect to Coproducts III. The powerset functor $\mathcal{P}_{!}$ of Item 3 of Proposition 2.4.3.1.4 has a symmetric strong monoidal structure
   \[ \webleft (\mathcal{P}_{!},\mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{!},\mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{!|\mathbb {1}}\webright ) \colon \webleft (\mathsf{Sets},\times ,\text{pt}\webright ) \to \webleft (\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\emptyset \webright ) \]

   being equipped with isomorphisms

   \[ \begin{gathered} \mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{!|X,Y} \colon \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright ) \xrightarrow {\cong }\mathcal{P}\webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright ),\\ \mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{!|\mathbb {1}} \colon \text{pt}\xrightarrow {\cong }\mathcal{P}\webleft (\emptyset \webright ), \end{gathered} \]

   natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.

4. Symmetric Lax Monoidality With Respect to Products I. The powerset functor $\mathcal{P}_{*}$ of Item 1 of Proposition 2.4.3.1.4 has a symmetric lax monoidal structure
   \[ \webleft (\mathcal{P}_{*},\mathcal{P}^{\otimes }_{*},\mathcal{P}^{\otimes }_{*|\mathbb {1}}\webright ) \colon \webleft (\mathsf{Sets},\times ,\text{pt}\webright ) \to \webleft (\mathsf{Sets},\times ,\text{pt}\webright ) \]

   being equipped with morphisms

   \[ \begin{gathered} \mathcal{P}^{\times }_{*|X,Y} \colon \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright ) \to \mathcal{P}\webleft (X\times Y\webright ),\\ \mathcal{P}^{\times }_{*|\mathbb {1}} \colon \text{pt}\to \mathcal{P}\webleft (\text{pt}\webright ), \end{gathered} \]

   natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, where

   • The map $\mathcal{P}^{\times }_{*|X,Y}$ is given by
     \[ \mathcal{P}^{\times }_{*|X,Y}\webleft (U,V\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}U\times V \]

     for each $\webleft (U,V\webright )\in \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright )$,

   • The map $\mathcal{P}^{\times }_{*|\mathbb {1}}$ is given by
     \[ \mathcal{P}^{\times }_{*|\mathbb {1}}\webleft (\star \webright )=\text{pt}. \]

5. Symmetric Lax Monoidality With Respect to Products II. The powerset functor $\mathcal{P}^{-1}$ of Item 2 of Proposition 2.4.3.1.4 has a symmetric lax monoidal structure
   \[ \webleft (\mathcal{P}^{-1},\mathcal{P}^{-1|\otimes },\mathcal{P}^{-1|\otimes }_{\mathbb {1}}\webright ) \colon \webleft (\mathsf{Sets}^{\mathsf{op}},\times ^{\mathsf{op}},\text{pt}\webright ) \to \webleft (\mathsf{Sets},\times ,\text{pt}\webright ) \]

   being equipped with morphisms

   \[ \begin{gathered} \mathcal{P}^{-1|\times }_{X,Y} \colon \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright ) \to \mathcal{P}\webleft (X\times Y\webright ),\\ \mathcal{P}^{\times }_{\mathbb {1}} \colon \text{pt}\to \mathcal{P}\webleft (\emptyset \webright ), \end{gathered} \]

   natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, defined as in Item 4.

6. Symmetric Lax Monoidality With Respect to Products III. The powerset functor $\mathcal{P}_{!}$ of Item 3 of Proposition 2.4.3.1.4 has a symmetric lax monoidal structure
   \[ \webleft (\mathcal{P}_{!},\mathcal{P}^{\otimes }_{!},\mathcal{P}^{\otimes }_{!|\mathbb {1}}\webright ) \colon \webleft (\mathsf{Sets},\times ,\text{pt}\webright ) \to \webleft (\mathsf{Sets},\times ,\text{pt}\webright ) \]

   being equipped with morphisms

   \[ \begin{gathered} \mathcal{P}^{\times }_{!|X,Y} \colon \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright ) \to \mathcal{P}\webleft (X\times Y\webright ),\\ \mathcal{P}^{\times }_{!|\mathbb {1}} \colon \text{pt}\to \mathcal{P}\webleft (\emptyset \webright ), \end{gathered} \]

   natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, defined as in Item 4.

Let $X$ be a set.

1. Powersets as Sets of Functions I. The assignment $U\mapsto \chi _{U}$ defines a bijection
   \[ \chi _{\webleft (-\webright )} \colon \mathcal{P}\webleft (X\webright ) \xrightarrow {\cong }\mathsf{Sets}\webleft (X,\{ \mathsf{t},\mathsf{f}\} \webright ), \]

   for each $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.

2. Powersets as Sets of Functions II. The bijection
   \[ \mathcal{P}\webleft (X\webright )\cong \mathsf{Sets}\webleft (X,\{ \mathsf{t},\mathsf{f}\} \webright ) \]

   of Item 1 is natural in $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, refining to a natural isomorphism of functors

   \[ \mathcal{P}^{-1}\cong \mathsf{Sets}\webleft (-,\{ \mathsf{t},\mathsf{f}\} \webright ). \]
3. Powersets as Sets of Relations. We have bijections
   \begin{align*} \mathcal{P}\webleft (X\webright ) & \cong \mathrm{Rel}\webleft (\text{pt},X\webright ),\\ \mathcal{P}\webleft (X\webright ) & \cong \mathrm{Rel}\webleft (X,\text{pt}\webright ), \end{align*}

   natural in $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.

Let $X$ be a set.

1. Universal Property. The pair $\webleft (\mathcal{P}\webleft (X\webright ),\chi _{\webleft (-\webright )}\webright )$ consisting of
   • The powerset $\mathcal{P}\webleft (X\webright )$ of $X$;
   • The characteristic embedding $\chi _{\webleft (-\webright )}\colon X\hookrightarrow \mathcal{P}\webleft (X\webright )$ of $X$ into $\mathcal{P}\webleft (X\webright )$;
   satisfies the following universal property:
   • Given another pair $\webleft (Y,f\webright )$ consisting of
     • A cocomplete poset $\webleft (Y,\preceq \webright )$;
     • A function $f\colon X\to Y$;
     there exists a unique cocontinuous morphism of posets
     \[ \webleft (\mathcal{P}\webleft (X\webright ),\subset \webright )\overset {\exists !}{\to }\webleft (Y,\preceq \webright ) \]

     making the diagram

     

     commute.

2. Adjointness. We have an adjunction^[3]
   
   witnessed by a bijection
   \[ \mathsf{Pos}^{\mathsf{cocomp.}}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright ) \cong \mathsf{Sets}\webleft (X,Y\webright ), \]

   natural in $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ and $\webleft (Y,\preceq \webright )\in \text{Obj}\webleft (\mathsf{Pos}^{\mathsf{cocomp.}}\webright )$, where the maps witnessing this bijection are given by

   • The map
     \[ \chi ^{*}_{X} \colon \mathsf{Pos}^{\mathsf{cocomp.}}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright ) \to \mathsf{Sets}\webleft (X,Y\webright ) \]

     defined by

     \[ \chi ^{*}_{X}\webleft (f\webright ) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f\circ \chi _{X}, \]

     i.e. by sending a cocontinuous morphism of posets $f\colon \mathcal{P}\webleft (X\webright )\to Y$ to the composition

     \[ X \overset {\chi _{X}}{\hookrightarrow } \mathcal{P}\webleft (X\webright ) \overset {f}{\to } Y. \]

   • The map
     \[ \text{Lan}_{\chi _{X}} \colon \mathsf{Sets}\webleft (X,Y\webright ) \to \mathsf{Pos}^{\mathsf{cocomp.}}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright ) \]

     is given by sending a function $f\colon X\to Y$ to its left Kan extension along $\chi _{X}$,

     
     Moreover, $\text{Lan}_{\chi _{X}}\webleft (f\webright )$ can be explicitly computed by

     $\displaystyle \webleft [\text{Lan}_{\chi _{X}}\webleft (f\webright )\webright ]\webleft (U\webright ) \cong \int ^{x\in X}\chi _{\mathcal{P}\webleft (X\webright )}\webleft (\chi _{x},U\webright )\odot f\webleft (x\webright )$

     $\displaystyle \phantom{\webleft [\text{Lan}_{\chi _{X}}\webleft (f\webright )\webright ]\webleft (U\webright )} \cong \rlap {\int ^{x\in X}\chi _{U}\webleft (x\webright )\odot f\webleft (x\webright )}\phantom{\int ^{x\in X}\chi _{\mathcal{P}\webleft (X\webright )}\webleft (\chi _{x},U\webright )\odot f\webleft (x\webright )}$

     (by Proposition 2.4.2.1.1)

     $\displaystyle \phantom{\webleft [\text{Lan}_{\chi _{X}}\webleft (f\webright )\webright ]\webleft (U\webright )} \cong \rlap {\bigvee _{x\in X}\webleft (\chi _{U}\webleft (x\webright )\odot f\webleft (x\webright )\webright )}\phantom{\int ^{x\in X}\chi _{\mathcal{P}\webleft (X\webright )}\webleft (\chi _{x},U\webright )\odot f\webleft (x\webright )}$

     for each $U\in \mathcal{P}\webleft (X\webright )$, where:

     • $\bigvee $ is the join in $\webleft (Y,\preceq \webright )$.
     • We have
       \begin{align*} \mathsf{true}\odot f\webleft (x\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f\webleft (x\webright ),\\ \mathsf{false}\odot f\webleft (x\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\varnothing _{Y}, \end{align*}

       where $\varnothing _{Y}$ is the minimal element of $\webleft (Y,\preceq \webright )$.