This is a follow-on from this question, where I pondered the consistency strength of Coq. This was too broad a question, so here is one more focussed. Rather, two more focussed questions:

I've read that CIC (the Calculus of Inductive Constructions) is interpretable in set theory (IZFU - intuitionistic ZF with universes I believe). Is there a tighter result?

And

What is the general consensus of the relative consistency of constructive logics anyway?

I am familiar, in a rough-and-ready way, with the concept of consistency strength in set theory, but more so of the 'logical strength' one has in category theory, where one considers models of theories in various categories. Famously, intuitionistic logic turns up as the internal logic of a topos, but perhaps this is an entirely different dimension of logical strength.

I guess one reason for bringing this up is the recent discussion on the fom mailing list about consistency of PA - Harvey Friedman tells us that $Con(PA)$ is equivalent to 15 (or so) completely innocuous combinatorial statements (none of which were detailed - if someone could point me to them, I'd be grateful), together with a version of Bolzano-Weierstrass for $\mathbb{Q}\_{[0,1]} = \mathbb{Q} \cap [0,1]$ every sequence in $\mathbb{Q}_{[0,1]}$ has a Cauchy subsequence with a specified sequence of 'epsilons', namely $1/n$). A constructive proof of this result would be IMHO very strong evidence for the consistency of PA, if people are worried about that.