The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Andrew McCreight wrote:
> I could be wrong, but this looks very similar to a question that was 
> asked a few years ago:
>
> http://coq.inria.fr/mailing-lists/coqclub/200201/msg00001.html
>
> In short, the answer was no.

I think that post only says definitively that injectivity isn't a 
theorem.  I'm interested in whether CIC + injectivity for Dyn is 
consistent, which is a different question.  It looks like the poster in 
the message you referenced wasn't sure of the answer to that question.

> On Mon, Jun 9, 2008 at 3:37 PM, Adam Chlipala <adamc AT hcoop.net 
> <mailto:adamc AT hcoop.net>> wrote:
>
>     Does anyone know if it would be consistent with (impredicative
>     Set) CIC to assert the injectivity of the [Dyn] constructor below
>     as an axiom?
>
>     Inductive dynamic : Set :=
>      | Dyn : forall T, T -> dynamic.