First, where you say "intensionality", you mean "extensionality" and specifically "function extensionality".
The Wikipedia page on Diaconescu's theorem uses the axiom of extensionality for sets which states that for sets $S$ and $T$, $S=T\iff(\forall x\in S.x\in T)\land(\forall x\in T.x\in S)$. It also mentions (without clear citation) that the reason Diaconescu's theorem doesn't apply to constructive type theories because they don't have an analogue of the axiom of separation.
Constructive type theories don't necessarily have a subobject classifier. Sometimes, e.g. in the Calculus of Constructions, there is a type $\mathsf{Prop}$ that is closely related to a subobject classifier. In HoTT, as described in section 3.5 of the HoTT book, we can defined a type $\mathsf{Prop}_{\mathcal U}$ via $\sum_{A:\mathcal U}\mathsf{isProp}(A)$. If we assume a propositional resizing axiom, we can define $\Omega\equiv\mathsf{Prop}_{\mathcal{U}_0}$ which will be of type $\mathcal{U}$ for any $\mathcal U$ which is a larger universe than $\mathcal{U}_0$. This behaves more like a subobject classifier. At this point the HoTT book references section 10.1.4 which asks whether the the category of sets (i.e. $0$-types in $\mathcal U$) defined in Chapter 9 is an elementary topos, i.e. whether it has a subobject classifier. $\mathsf{Prop}_{\mathcal U}$ would almost work except that it is "too big" to be of type $\mathcal U$, but propositional resizing would allow us to use $\Omega$ which is of type $\mathcal U$. The very next section presents Diaconescu's theorem in this context. It is based on the presentation of the Axiom of Choice in section 3.8.
The Axiom of Choice in section 3.8 is different from the provable type-theoretic "axiom" of choice described earlier in the book in section 1.6. One way to think about the difference between classical and constructive logic is that constructive logic introduces new logical connectives: the constructive disjunction and the constructive existential. (Edward Nelson describes it this way, it is also evident in categorical semantics for classical logic, and is also explicit at the end of section 3.7 where $P\lor Q$ and $\exists x:X.P(x)$ are defined as $||P+Q||$ and $||\sum_{x:X}P(x)||$ respectively.) So the question of which notion of existential to use when formulating the Axiom of Choice is significant. If we use the "constructive existential", i.e. the dependent sum, then we get the type-theoretic "axiom" of choice. If we use the "classical existential", i.e. the propositional truncation of the dependent sum (of a family of mere propositions), we get something that behaves like the traditional axiom of choice (and which is not provable) including leading to Diaconescu's theorem. What Diaconescu used is the usual formulation in category theory, namely that all epimorphisms are split. One could imagine formalizing this as $\prod_{A,B:\mathcal U}\prod_{f:A\to B}(\prod_{b:B}\sum_{a:A}f(a)=b)\to\sum_{g:B\to A}\prod_{a:A}f(g(a))=a$, but this is an internal statement and "all epimorphisms are split" is an external statement and there's no reason to expect the internal statement to mirror the external one (and, again, we would have to decide whether we want $\Sigma$ or $\exists$).
So, all told, the type-theoretic "axiom" of choice is not obviously the appropriate internal formulation of the axiom of choice (in fact, I think most would say it's obviously not the appropriate internal formulation), Diaconescu isn't utilizing an internal formulation anyway, and further Diaconescu was talking about elementary ($1$-)toposes while the intended models of HoTT are $(\infty,1)$-toposes. In particular, subobjects seem much less informative about higher categorical structure and indeed in the HoTT book the Axiom of Choice is limited to types with low h-level and it only talks about Diaconescu's theorem with respect to these low h-level types.
As a final note, there are Curry-Howard-style correspondences to classical proof systems, notably the $\lambda\mu$-calculus of Parigot which is given a categorical semantics in the paper I previously mentioned.
