[Agda] Agda with excluded middle is inconsistent

[Nils Anders Danielsson]

On 2010-01-08 12:05, Noam Zeilberger wrote:
> In intuitionistic second-order logic you can prove ∀ P.~~(P \/ ~P),
> but not ~~(∀ P. P \/ ~P).

If you allow bar recursion you can prove some double-negation shift
lemma. I suspect that this means that a sufficiently strong variant of
bar recursion is not compatible with injective type constructors.

--
/NAD