The right text to look at for more details is Andrej Bauer's text "Propositions as [Types]". You may also look at the paragraph "In Type Theory" of this nLab article, which explains the issue well. I can only speak about extensional type theory and its relation to categories and intuitionistic logic, since I do not have much experience with intensional type theory and HoTT.
The confusion comes from the fact that there are two ways to make "propositions as types" precise. Let me call the first one "proposition as proof-relevant types" and the second one "propositions as subsingelton types". In the nLab article they are called "propositions as all types" and "propositions as some types" respectively.
In the "proposition as proof-relevant types" world the existence quantifier corresponds to strong $\Sigma$-types. In that world something which looks like an axiom of choice is indeed valid. But there is no direct correspondence between the "propositions as proof-relevant types" logic and that what is normaly considered to be first-order many sorted intuitionistic logic. In particular, the proof of Diaconescu's theorem does not go through.
The kind of type theoretic logic that corresponds more directly to standard intuitionistic many-sorted first-order logic is the "propositions as subsingelton types" (or proof-irrelevant types) interpretation. This is also the version that people mean when they speak of the internal language/logic of a category. In that version the analogue of the axiom of choice is not automatically valid. More about that later.
Propositions as proof-relevant types
Extensional Martin-Löf dependent type theory comes per default with $\mathbf 1, \Sigma, \Pi$ and extensional equality. Let us look at an example to understand what "propositions as types" means. Consider the type
$$\Pi m :\mathbb N.\Sigma n:\mathbb N.n>m$$
This type should intuitively be the type of proofs of the proposition "for all natural numbers $m$ there is a natural number $n$ such that $n$ is greater than $m$". Let me construct a term of that type. Say we already have a proof of the fact that for each $m:\mathbb N$ the natural number $S m$ is larger than $m$, where $S$ denotes the successor function. In the propositions as types language this means that we have a term $p: \Pi m:\mathbb N.Sm>m$. Then the following term will be "a proof" of the proposition we like to prove.
$$ \lambda m.(Sm,p m): \Pi m:\mathbb N.\Sigma n:\mathbb N.n>m$$ Now when we have an actual natural number, for example $S0$, then we can apply our proof term to that number.
$$(\lambda m.(Sm,p m))(S0) \equiv (SS 0, p(S0)) : \Sigma n:\mathbb N. n>S0$$
Here I use the $\equiv$-sign to denote judgemental equality. It is okay to understand this as "equal by definition" or "almost syntactically equal" from the categorical perspective, I hope no computer-scientist will kill me. We can now extract two components from the term of $\Sigma n:\mathbb N. n>S0$. The first component is a natural number $(SS0,p(S0)).1 \equiv SS0$, and the second component is a proof $(SS0,p(S0)).2 \equiv p(S0) : SS0 > S0$ of the fact that the natural number $SS0$ which we obtained from the first component is actually larger than the number $S0$ we started with. You can imagine that all types can be understood both as structures and as propositions. By inhabiting a type you do at the same time prove something. For example proving that prime numbers exist is arguably constructively the same activity as finding an inhabitent of the type of prime numbers.
The main point I am trying to make is that if $x:X\vdash Y\text{ type}$ is a dependent type (= a formula on $X$), then showing that "there is $x:X$ such that $Y(x)$ holds" is the same thing as inhabiting $\Sigma x:X.Y$. To do that we have to provide a term $t:X$ and a proof $p:Y[t/x]$. The pair $(t,p)$ will then be of type $\Sigma x:X.Y$. On the other hand, and this is crucially, we are able to extract from each proof $t:\Sigma x:X.Y$ both a term $t.1:X$ and a proof $t.2:Y[t.1/x]$ of the fact that $Y$ holds for $t.1$. This is exactly what won't be possible in the "proposition as subsingelton types" interpretation of logic.
Now what shall the axiom of choice be in this setting. Something which is reasonable (and works even without type theoretic universes) is the following "axiom scheme" (it is more a meta-property of the system than an actual axiom scheme).
(TTAC) Assume that $x:X\vdash Y \text{ type}$ is a family of types depending on another type $X$. If we can show that each $Y(x)$ is inhabited, then we may produce a choice function which chooses for each $x:X$ an element of $Y(x)$. This means we can produce a term of type $$(\Pi x:X.\Sigma
y:Y(x).\mathbf 1)\to (\Pi x:X. Y(x))$$
The "type theoretic axiom of choice" in this version is just true. One can easily check that the judgement below is correct.
$$\lambda p. \lambda x. (p\, x).1 : (\Pi x:X.\Sigma
y:Y(x).\mathbf 1)\to (\Pi x:X. Y(x))$$
I have put "axiom of choice" in quotation, since its categorical semantic isn't really what category theorists understand as the axiom of choice in a category. When our type theory has a universe $\mathcal U$, then another statement which looks reasonably like the axiom of choice is that the type $$\Pi X:\mathcal U. \Pi (Y:X\to \mathcal U). ((\Pi x:X.\Sigma
y:Y\, x.\mathbf 1)\to (\Pi x:X. Y\,x))$$
is inhabited. But this is also just true, and it is not hard to produce a term of that type. This article here from the standford encylopedia of philosophy suggest that we should call the fact that we can always find an inhabitend of $$\Pi x:X.\Sigma y:Y. P(x,y)\to (\Sigma f:(X\to Y).\Pi x:X.P(x,f x))$$
the type theoretic axiom of choice. I am not exactly sure why, but as in the cases before, it is not hard to produce a term of that type!
Why does the type theoretic axiom of choice not imply the law of excluded middle? Well, we can look at a proof of Diaconescu's theorem and try to find out where we can no longer follow. When we go to section 3.7 of the article here (Intuitionism in the Philosophy of Mathematics - Standford Philosophy Encyclopedia) then we see that we have to form a "subset type" in the first step. What are subsets in type theory? Given some type $X$ and a predicate $x:X\vdash P(x) \text{ type}$ ranging over it, we like to form the type $\vdash \{x:X|P(x)\} \text{ type}$ of all $x:X$ which satisfy $P(x)$. So far we have no way of doing this. What maybe comes closest is the type $\Sigma x:X.P(x)$. After all, to produce a term of that type we need to provide at a term $t:X$ and a proof $p: P(t)$ that $t$ satisfies $P(t)$. But there is a problem: two different proofs $p,p':P(t)$ will give us distinct terms $(x,p)$ and $(x,p')$ of $\Sigma x:X.P(x)$, even though the element $x$ should really just appear once in the subset types. What we need is a mean is to somehow collapse the fibers of $P(x)$, so that for each $x:X$ the type $P(x)$ can have at most one term. Such a type is called a subsingelton type (or mono-type or mere proposition), and the process of collapsing the fibers of a type so that it becomes a mere proposition $[P(x)]$ is known under the name propositional truncation in type theory. The brackets [-] are a new type constructor whose rules in extensional type theory are described in Bauer's text which I mentioned at the beginning. The subset type is $\Sigma x:X.[P(x)]$. Let us now speak about the second type theoretic interpretation of logic.
Proposition as subsingelton types
This is a proof-irrelevant logic. Propositions are those types which contain at most one term. One says that a dependent type $\Gamma\vdash P \text{ type}$ is a subsingelton type when $$\Gamma, p:P,q:P\vdash p \equiv q:P$$
holds, i.e. when all terms of $P$ are judgementally equal. This makes sense because the judgementally equality sign $\equiv$ is part of the formal deductive system of Martin-Löf Type Theory. In the categorical semantic a type $\Gamma \vdash A\text{ type}$ is a subsingelton type if and only if the display map $p_A:\Gamma.A\to \Gamma$ of that type is a monomorphism. In the set-theoretic semantic of type theory $P$ is a subsingelton type if and only if each of its fibers contains at most one element. The type constructors $\Pi,\to$ and $=$ turn subsingelton types into subsingelton types, so we can still use them in the same way to interpret logic in type theory. The dependent sum type $\Sigma$ does not. Hence, to get a propositional truncated version $\exists$ of the existential quantifier, we need to always apply [-] after we apply $\Sigma$. For example the proof-irrelevant type-theoretical implementation of the proposition "for all $m:\mathbb N$ there is $n:\mathbb N$ such that $n>m$" is now $$\Pi m:\mathbb N.[\Sigma n:\mathbb N. n>m]$$
To produce (the necessarily unique) term of that type we still need to provide for each $m:\mathbb N$ a term $t(m):\mathbb N$ and a proof that $t(m)$ is greater than $m$. But we will no longer be able to extract from a proof of $\forall m:\mathbb N.\exists n:\mathbb N.n>m$ a function which provides such $n$s! The propositional truncation prevents this, the information is lost. How does "the axiom of choice" look like in this setting? A first version is the following axiom scheme.
(EAC) Whenever we have a dependent type $x:X \vdash Y(y)\text{ type}$ such that the subsingelton type $\forall x:X. \exists y:Y(x).\top$ is inhabited, then we may produce a term of type $\Pi x:X.Y(x)$.
The categorical semantic of that axiom scheme in a category is known under the name "external axiom of choice". "External" because the quantifiers which range over the sets $X$ and $Y$ come from the outside.
The categorical semantic of $\forall x:X.\exists y:Y(x).\top$ is that the image of the display map $p_Y: X.Y\to X$ is an epimorphism. A term of $\Pi x:X.Y(x)$ is the same thing as a section of the display map. Hence we see that (EAC) is valid in a category (with enough structure) when every regular epimorphism splits. When we have a meta-set-theory such as ZFC, then we will be able that EAC is valid in any category $Set_\kappa$ of sets up to a certain size, but when we work in a set theory without choice, such as ZF, then we will not be able that $Set_\kappa$ validates the external axiom of choice EAC for each cardinal. In particular this shows that the axiom of choice in the EAC version is not automatically valid in extensional type theory.
Remark. There is also an internal axiom of choice (IAC), where we also internalize the quantification over sets. To explain its meaning we would have to either introduce universes or the stack semantic of Mike Shulman, which is probably unnecessary to get the point across. The internal axiom of choice is weaker than EAC, but proving that the categories $Set_\kappa$ satisfy IAC does again require some amount of choice in the meta-set-theory.
Arguably, the axioms (EAC) and (IAC) correspond more closely to what we call "the axiom of choice" in set-theory. This is also witnessed by the fact that the categories $Set_\kappa$ always satisfy the type theoretic axiom of choice TTAC (as so does any other topos), but that the validity of EAC and IAC in $Set_\kappa$ depends on some amount of choice in the meta-theory. You can find a detailed comparison between the choice axioms in material set theory and choice in type theory in Mike Shulman's paper Stack Semantics and the Comparison of Material and Structural Set Theories. To read more about IAC and EAC you may look at the nLab article about choice.
Informal summary.
To prove constructively that each fiber of a family of sets is inhabited, you have to write down a method which produces inhabitants of the fibers for any given index. When you still remember your method of producing those inhabitants, then you are of course able to produce a choice function. This is the situation where "exists" is modeled through $\Sigma$-types. On the other hand, when you do not have access to the method and only know that a constructive proof exist (for example because another mathematician has announced that they have produced a constructive proof, but they are unwilling to publish it), then you can not write down a choice function constructively. This is the situation where your only information is that a proof exists, but all other information is lost (propositional truncation).
Best Answer
The axiom of choice, as far as 2019, and as far as "standard foundations" go, is an axiom of set theory, which is a foundation of mathematics.
You could argue that the power set axiom "just sits there in the background, lurking about, doing nothing but scaring those poor predicativists", because you use it to prove that uncountable sets exist.
Historically, however, Zermelo is known to have viewed choice as a logical principle. It can be seen as an inference rule, and this is how some second-order set theoretic proof assistant will prove choice in that sort of manner.
Regardless, progression in mathematics since 1904 moved the axiom of choice from an inference rule to a set theoretic axiom.
To the edit about group theory. Let's review for a moment where we actually need the axiom of choice in group theoretic proofs.
Since the axioms of a group cannot even decide if a model has some finite number of element, there are infinite models of any size. The axiom of choice comes in when we want to say something like "Every set carries a group structure" (which is equivalent to the axiom of choice). But this is not a statement in the language of groups, it's not even a statement about groups. It's a statement about sets.
Okay, so maybe the axiom of choice enters when we want to say that every divisible abelian group is injective, or every free abelian group is projective. Those are each equivalent to the axiom of choice. But again, these is not a statement in the language of groups. This is a "meta-theorem" about groups. The properties of projectivity and injectivity are not first-order anymore, they quantify over other groups and group homomorphisms. So this is really not something where choice enters "in the logic", but rather that the statement "exceeds the logic".
So what about this, and about all those rings and vector spaces and whatnot? Well. As with many cases, the axiom of choice is needed to produce some coherent choices. If we restrict all our attention to countable groups (i.e., define "countably injective groups" as those satisfying injectivity when all the groups involved are countable, etc.) then the axiom of choice will not be necessary anymore.
Choice, as I often said, is used to make our statement neat. Even if we mostly (or only) care about countable objects, or countably generated objects, choice makes mathematics simpler. It lets us generalize things to "all infinite objects", rather than "all countable objects" or "all well-ordered objects".
Despite all that, it's still a set theoretic axiom, and it comes into action when you move from the first-order theory of something to statements which actively involve quantifying over all possible models of a theory.