# 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.
• How are you implementing $1=2$ in the calculus of constructions? In the calculus of inductive constructions, with objects of the inductive type nat, it certainly does imply False (the proof tactic in Coq is discriminate and the proof object is centered around a dependent pattern matching in the type 1=2). – Gilles 'SO- stop being evil' Nov 28 '17 at 21:25
• @paulotorrens: $2$ is some type-theoretic version of the two-element set $\{0,1\}$. With the standard (numeric) partial order, this set becomes a lattice which happens to be complete (have suprema and infima of arbitrary subsets). Completeness only holds if some version of the law of excluded middle is available; a constructive substitute which is always complete is the lattice of all subsets of $\{\heartsuit\}$, which contains $\emptyset$ and $\{\heartsuit\}$ (corresponding to $0$ and $1$), but potentially also further elements. – Ingo Blechschmidt May 16 '18 at 20:06