TLWR : I'd like to define either $\operatorname{Hom}_F : \text{Set} \times \text{Set}_* \to \text{Set}_*$ (set of functions with finite support) or simply $\mathcal{P}_F : \text{Set} \to \text{Set}$ (set of finite subsets) via (useful) universal properties.
More generally I struggle with the notion of finiteness of an object, since it seems the only definition I have is "not infinite" which is not really constructive.
Here I denote $\text{Set}_*$ the category of pointed sets $(X,x)$ with $x \in X$ and with morphims functions respecting the pointed element. (There is nothing special about sets but we ought to start somewhere).
Given $(Y,y)$ a pointed set, and $X$ a regular set, a function $f: X \to Y$ is with finite support if it is constant equal to $y$ outside of some finite subset $K$ of $X$. Among functions with finite support there is one particular function : the constant function to $y$, which we could call the null function. It endows the set of functions with finite support $X \to (Y,y)$ with a distinguished element making it a pointed set : $\operatorname{Hom}_F(X,(Y,y))$.
Similar to the usual adjunction there is an isomorphism $\operatorname{Hom}_F(A \times B,(C,c)) \simeq \operatorname{Hom}_F(A, \operatorname{Hom}_F(B,(C,c)))$. However it does not yields natural transformations $\eta_{B,C}: B \times \operatorname{Hom}_F(B,(C,c)) \to C$ and $\epsilon_{A,B} : A \to \operatorname{Hom}_F(B,(A\times B,(a,b)))$ since the identity is not in $\operatorname{Hom}_F(X,X)$ when $X$ is infinite. The best we have is a family of such maps parametrized by finite subsets of $\operatorname{Hom}_F(B,(C,c))$ or $A \times B$.
So I tried to define $\mathcal{P}_F(X)$ the set of finite subsets of $X$. Such subset $K$ corresponds to a map $\chi_K: X \to \textbf{2}$ which satisfies : Any map $f : \mathbb{N} \to X$ such that the composite $\chi_K \circ f$ si constant to $\textbf{1}$ is not injective. Yet I'm stuck trying to translate "not injective" (not mono). I'm not very well aware of constructive mathematics, but I feel there is not easy way to say that two elements (or two maps) are distincts.
Is there a right way to define such objects/notions ? If yes, is there a way to define it without using a natural number object ?
Thank you, i apologize for my English.