The Coq mailing list

[Noam Zeilberger <noam.zeilberger AT gmail.com>]

On Thu, Jan 7, 2010 at 4:15 PM, Thorsten Altenkirch 
<txa AT cs.nott.ac.uk>
 wrote:
>> ...I'm not sure about this expansion, and the analogy.  I think the
>> question is whether we view the declaration of type constructors in
>> the same way that we view the declaration of term constructors (i.e.,
>> as stipulating a new way of constructing things, in this case
>> inhabitants of Set).  If we do, then type constructors are by
>> definition injective.
>
> I don't see the analogy. A term constructor is injective because an 
> inductive type is freely generated from constructors. Indeed, we can show 
> that the structure map of an initial algebra is an isomorphism and hence 
> injective. However the universe of sets is not freely constructed from type 
> constructors but they are really definitions.

But freeness ("inductive type = no confusion + no junk") is only a
sufficient condition, right?  Injectivity = no confusion.

> We should justify principles like this (i.e. all type constructors are 
> injective) by a semantic explanation or by a translation into a well 
> understood core language e.g. (extensional) Marttin-Loef Type Theory with 
> W-types and universes. I don't know any such explanation which would 
> justify this principle. Moreover, Chung's example shows that this is not 
> possible (without giving up something else) since pure type theory is 
> consistent with EM.

Agreed that there should be a convincing explanation, but again, I do
think there is a strong intuition behind the principle (what Dan Doel
and I were getting at), and the fact that it plays an important role
in typechecking suggests that we shouldn't jump to conclusions.  I am
not sure that Agda should be conservative over classical mathematics:
it seems there is a fundamental tension between exploiting the full
power of a constructive type theory and upholding the fictions of
classical mathematics.  Chung-Kil's paradox shows that you can't
reason classically in Agda just by adding the law of excluded middle
-- okay, so don't do it that way.

Could you explain what you meant by: "Also while we may accept that
extensions of Type Theory may be anticlassical, we should expect that
core Type Theory is consistent with EM."?

Noam
_______________________________________________
Agda mailing list
Agda AT lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda