Trivializations of set-theoretic fiber bundles up to permutations

Question

Let $A,B$ be sets with $|A|=n=k \cdot m$ and $|B|=m$. Let $\pi: A \twoheadrightarrow B$ be a surjective map, s.t. $|\pi^{-1}(b)|=k$ for all $b \in B$. I am basically interested in trivializations $\alpha: A \cong B \times [k]$, but only almost. Actually, I would like to identify those $\alpha$'s that have the same SET of preimages $S_{\alpha}=\{\,\alpha^{-1}\left(B\times \{i\}\right) \, | \, i \in [k] \,\}$.

It's easy to compute the number of trivializations up to this identification. I am actually looking for a nicer set-up, so that the identification is kind of "built-in". I thought about exchanging $[k]$ by a multiset with $k$ non-distinguishable elements, but I am not sure if this makes sense.. Do you see an elegant (read "categorical"/"natural") way to define trivialitations up to $S_k$-action (basically an unordered version of the above)?

Answer 1

Working in univalent type theory, you could define your type of trivialisations as $$\sum_{(C : BS_k)} \sum_{(\alpha : A \simeq B \times C)} \pi_1 \circ \alpha = \pi$$ where $BS_k = \sum_{X : \mathcal{U}} \| X \simeq [k] \|$ is the type of $k$-element types. This naturally endows the type of trivialisations $A \simeq B \times [k]$ with an action of $S_k$. (Alternatively you could just require $C : \mathcal{U}$, since the fact that $C$ has $k$ elements follows from the assumptions. $\sum_{C : \mathcal{U}} A \simeq B \times C$ is the type of lenses from $A$ to $B$.)

Answer 2

Naïm Favier gave a nice answer in terms of univalent types. A more "down-to-earth" definition could be the following: A unordered trivialization is an unordered $k$-partition $\{A_1,\dots,A_k\}$ of $A$ s.t. the $\pi\circ \iota_i:A_i \to B$ are bijections.