Finite semisimple module categories are separable algebra modules

Choose $m$ as in F1, construct $A=[m,m]$, and use the stated comparison $\mathcal{M}\simeq {\mathrm{Mod}}^l(A)$. Concretely its multiplication is the unique map $\mu :A\otimes A\to A$ representing $m\odot (A\otimes A)\to (m\odot A)\odot A\to m\odot A\to m$, the last two maps being evaluation; hence on ordinary endomorphisms $a\cdot b=b\circ a$. Its unit represents $1_m$. F1 proves associativity, unitality, the left action on $[m,n]$, and right module compatibility by the two rigidity adjunctions, and proves full faithfulness and surjectivity using exact internal Homs and free presentations. In particular the category of left $A$-modules is finite semisimple before any separability assertion is made.

On this left module category let $S(P)=A\otimes U(P)$, with the free action on the first factor, where $U$ forgets the action. There is a module-natural epimorphism $r:S\to \mathrm{Id}$ with $r_P=l_P$, the action on $P$. Epimorphy follows because $l_P(\eta \otimes 1)=1$ on underlying objects, and kernels and cokernels of $A$-module maps are inherited from $\mathcal{C}$. This assertion does not require the displayed underlying section to be $A$-linear. Choose representatives $p$ of the finitely many simple left $A$-modules. Since that module category is semisimple, choose an $A$-linear section $j_p:p\to S(p)$ of $r_p$. Extend these sections by additive decomposition to an ordinary natural transformation $t:\mathrm{Id}\to S$: on $P={⨁}_p{\mathrm{Hom}}_A(p,P)\otimes p$, take the direct sum of the corresponding maps $j_p$ and transport using the canonical evaluation decomposition. Its naturality follows because any map is a matrix on the multiplicity spaces. By construction $rt=1$.

Apply the explicit averaging in F2 to $t$ and set $s=\mathrm{Av}(t)$. Then $s$ is module-natural and $rs=1$. Define the requested separability section by ${\sigma }_A=s_A:A\to S(A)=A\otimes A$. Every component of $s$ is a left $A$-module map, so ${\sigma }_A$ is left $A$-linear. It is also right $A$-linear: naturality of $s$ at the left $A$-map $\mu :A\otimes A\to A$ gives $S(\mu )s_{A\otimes A}=s_A\mu$. Module-naturality identifies $s_{A\otimes A}=s_A\otimes 1_A$, and $S(\mu )=1_A\otimes \mu$, so $(1_A\otimes \mu )({\sigma }_A\otimes 1_A)={\sigma }_A\mu$. Finally $r_A{\sigma }_A=1_A$ is $\mu {\sigma }_A=1_A$. This constructs an actual bimodule section; it uses finitely many chosen sections and the fixed normalized canonical separability element, without requiring a pivotal or spherical structure on $\mathcal{C}$. Thus $A$ is separable.

For another finite semisimple right module category represented by $B$, F1 identifies every right exact module functor with $Q{\otimes }_A-$ for $Q=F(A)$ a $B$-$A$ bimodule, whose right action is $F(\mu )$ under $F(A\otimes A)\cong F(A)\otimes A$. Every linear functor between the semisimple categories here is exact, so there is no additional exactness restriction. F1 proves that the canonical free coequalizer of each module gives the natural isomorphism to this tensor functor, and that evaluation of transformations at $A$ and tensoring a bimodule map are inverse operations. This proves the full claimed equivalence and its precise orientation together with the separable-algebra construction.