Is impredicative Set consistent with the excluded middle?

While studying Coq, I found a few references that impredicative Set might not work well with classical axioms, in particular the axiom of choice.

I'm working on a dependent type system based on the calculus of constructions (with Prop and Set), on which I intend to add Peirce's law on sets, as in the computability side it represents call/cc (capturing/resuming the whole computation).

My question is: is the calculus of constructions* with an impredicative Set, with the excluded middle working on sets (precisely, forall P: Set, ((P -> False) -> P) -> P being of type Set), without the axiom of choice, consistent? I didn't manage to find a reference for that.

(* Would inductive types make any difference, from CoC to CIC?)

I'm not an expert, but my understating was not that it it was inconsistent, but that it implies proof irrelevance. That is, if $s,t:T$ then $s=t$.

This gives many undesirable properties, like having $1=2$, but I'm not sure it actually implies bottom.
This answer had similar details.

StackExchange Computer Science Q#84598, answer score: 2