[Agda] Agda with the excluded middle is inconsistent ?

[Benja Fallenstein]

Hi all,

On Thu, Jan 7, 2010 at 4:27 PM, Thorsten Altenkirch <txa at cs.nott.ac.uk> wrote:
>> [E]laboration into a core theory [...is...] really the
>> direction to go in (it seems to me), because trusting a core theory is much
>> easier than trusting that you've directly implemented all the sugar correctly.
>
> Indeed, this is my conclusion. The translation into a core language corresponds to a semantic justification of the principle. And without such a justification I don't see any reason why such a principle should be adopted. Just because it has been implemented by accident?

I've thought for a while that the slogan for this should be,
"metaprograms prove metatheorems." Although the literal interpretation
of that -- i.e., the translation into the core being in fact a
function in the core theory [with additional universe levels added if
needed] whose type is the metatheorem in question -- seems still a
little higher than we can reach at this point, alas...

- Benja