coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Consistency of axiom about dynamic packages?

From: Adam Chlipala <adamc AT hcoop.net>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Consistency of axiom about dynamic packages?
Date: Mon, 09 Jun 2008 18:37:57 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.

[Coq-Club] Consistency of axiom about dynamic packages?, Adam Chlipala
- Re: [Coq-Club] Consistency of axiom about dynamic packages?, Andrew McCreight
  - Re: [Coq-Club] Consistency of axiom about dynamic packages?, Adam Chlipala
    - Re: [Coq-Club] Consistency of axiom about dynamic packages?, Benjamin Pierce
      - Re: [Coq-Club] Consistency of axiom about dynamic packages?, Adam Chlipala
        
        Re: [Coq-Club] Consistency of axiom about dynamic packages?, Zhong Shao