coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>
- To: Noam Zeilberger <noam.zeilberger AT gmail.com>
- Cc: Chung Kil Hur <Chung-Kil.Hur AT pps.jussieu.fr>, coq-club AT inria.fr, Agda mailing list <agda AT lists.chalmers.se>
- Subject: [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent
- Date: Thu, 7 Jan 2010 15:15:34 +0000
Hi Noam,
>> Surely, type constructors should not be injective in general. A definition
>> of the form
>> data I : (Set -> Set) -> Set where
>> should be expandable by an annonymous declaration
>> I : (Set -> Set) -> Set
>> I F = data {}
>> in an analogous way a named function definition can be expanded by
>> definition and a lambda abstraction
>
> ...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.
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.
Cheers,
Thorsten
- [Coq-Club] [Agda] Agda with excluded middle is inconsistent, Chung Kil Hur
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Dan Doel
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
David Wahlstedt
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Andreas Abel
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Thorsten Altenkirch
Archive powered by MhonArc 2.6.16.