Is there a name for the exponential semiring of G-sets?
In an ordinary type system, the types are like sets.
It's possible to extend this analogy and get a $G$-type system where every type is acted on by a fixed group $G$ and these actions respect the type constructors $+, \times, \to$ and so on.
The Burnside semiring of a group $G$ looks a lot like a simple type system with products $ \times $ and coproducts $ + $.
This lecture by Richard Borcherds contains a construction of the Burnside semiring and later the Burnside ring.
This can be thought of as similar to a type system. The $G$-sets, $A_1 \cdots A_n$ are the irreducible transitive actions of $G$ on finite sets. They are analogous to primitive types.
$A+B = \{ (S^+, 1, a, (A, B)) : a \in A \} \cup \{ (S^+, 2, b, (A, B)) : b \in B \}$ is like a coproduct.
$A \times B = \{ (S^\times, a, b, (A, B)) : a \in A \land b \in B \}$ is like a product.
The group action is defined as follows:
$$g \triangleright (S^+, 1, a, (A, B))) = (S^+, 1, g \triangleright a, (A, B))$$
$$g \triangleright (S^+, 2, b, (A, B)) = (S^+, 2, g \triangleright b, (A, B))$$
$$ g \triangleright (S^\times, a, b, (A, B)) = (S^\times, g \triangleright a, g \triangleright b, (A, B)) $$
We can get a version of the simply typed lambda calculus by adding in $A \to B$.
$$ g \triangleright (S^\to, \{ \cdots (a, b) \cdots \}, (A, B)) = (S^\to, \{ \cdots (g \triangleright a, g^{-1} \triangleright b) \cdots \}, (A, B)) $$
Or equivalently $g \triangleright \lambda x \mathop. f(x) \longrightarrow \lambda x \mathop. g \triangleright f(g^{-1} \triangleright x)$.
We can show that this definition of conjugation for a function makes sense by examining $f : A \times B \to C$ and $h : A \to B \to C$.
$$ g \triangleright (f : A \times B \to C) \\ g \triangleright (\lambda (a, b) \mathop. c(a, b)) \\ (\lambda (a, b) \mathop. g \triangleright c(g^{-1} \triangleright a, g^{-1} \triangleright b))) $$
Which resembles
$$ g \triangleright ( h : A \to B \to C ) \\ g \triangleright (\lambda a \mathop. \lambda b \mathop. c(a, b)) \\ \lambda a \mathop. g \triangleright (\lambda b \mathop. c(g^{-1} \triangleright a, b) \\ \lambda a \mathop. \lambda b \mathop. g \triangleright c(g^{-1} \triangleright a, g^{-1} \triangleright b) $$
And also, conjugation treats the identity function correctly:
$$ g \triangleright \text{id} \\ g \triangleright (\lambda x \mathop. x) \\ (\lambda x \mathop. g \triangleright g^{-1} \triangleright x) \\ \lambda x \mathop. x $$