Does the definition of the fundamental group implicitly assume the Axiom of Choice? Okay, I'm a little foggy around the axiom of choice, so help me out here.
The standard way the fundamental group of a connected space $X$ is defined is as follows. You consider the set of all loops based at some point $x$. You define an equivalence relation called homotopy on the elements of this set, and the equivalence relation partitions the set into equivalence classes. Now you impose a group structure on these classes by identifying identity and defining multiplication this way: to multiply to classes $A$ and $B$, you pick out an element $a$ from $A$, and an element $b$ from $B$, and multiply the loops $a$ and $b$ and call the product of $A$ and $B$ as the equivalence class of $ab$
$$A \circ B = [a\cdot b]$$
However, picking out $a$ from $A$ and $b$ from $B$ sounds a lot like the statement of axiom of choice, which talks about picking out representative elements from disjoint sets.
So what's the deal here. I'm getting something wrong about the axiom of choice (very likely) or fundamental groups do require the axiom of choice.
Much obliged for your time and help.
 A: This is a known issue, and the way we go around it is in fact by showing that the operation of the group does not depend on the choice of representatives. This allows us to make all sort of computations with only choose two elements, at a time.
And choosing two elements from two non-empty sets is hardly a choice at all. It is simply repeating two instances of "existential instantiation", where we replace an existential quantifier by an object.
The axiom of choice is needed when you have infinitely many choices to make at once. And even this is just a general rule of thumb.

You can find similar definitions when defining the real numbers as equivalence classes of Cauchy sequences, or when defining cardinal arithmetics, or just when you usually define any type of function on a set and show that you can define an equivalence relation that this function can be "pulled" to the quotient set.
A: No, it's not using AC. You're just making two "choices" here - don't need AC for that, just the fact that a nonempty set has an element. You need AC when you need to make infinitely many "choices" "simultaneously".
Formally, AC says this: Say $X$ is a set, $P(X)$ is the power set, $F:S\to P(X)$ and $F(s)\ne\emptyset$ for every $s\in S$. Then there exists $f:S\to X$ such that $f(s)\in F(s)$ for all $s\in S$.
If $S$ is finite you don't need AC, that statement follows from the other axioms of set theory.

EDIT: At least one person has been confused by the connection between the formalisms here and in the OP. To be explicit, if not pedantic:
Suppose $A$ and $B$ are as in the OP. Rats, another notation conflict. Let's say the OP is talking about a topological space $\Omega$. Let $X$ be the set of all loops in $\Omega$ based at $x$. Then $A$ and $B$ are nonempty subsets of $X$.
Define $F:\{0,1\}\to P(X)$ by $F(0)=A$, $F(1)=B$. AC says there exists $f:\{0,1\}\to X$ with $f(j)\in F(j)$, $j=0,1$. But we don't need AC for that, we can say "let $f(0)=a\in A$ and let $f(1)=b\in B$".
Here $S=\{0,1\}$. If $S$ is infinite we can't define $f$ one element at a time, takes too long.
