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?)