coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] going from equality in Type to equality in Set

From: Avi Shinnar <shinnar AT eecs.harvard.edu>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] going from equality in Type to equality in Set
Date: Tue, 29 Sep 2009 11:06:05 -0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=W2CDa2V4j4yfWuiOvLuOt/tMgG/NqkFsluFL1TPurj8LcSa8kZJB4rgOmg92jsdQIb 1X3mYEIlHhIPEZB8ZYnYvpSkBPJSXK+/TBQu2kjgMKfACgkz+oMtHe3y0PCY8CI0Ouon X7uMYmmhdtPq1xQfTaULMNou5DexRrGy1VoOc=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi all,

Is it possible to prove the following lemma?

Lemma type_set_eq (A B:Set) : @eq Type A B -> @eq Set A B.

This came up because I have an inductive type
Inductive Evals : forall {A:Type} ...
and one of the constructors forces A to be a Set. So inversion on on
Evals object yields a type equality in Type over objects in Set.

Thanks,

Avi

[Coq-Club] going from equality in Type to equality in Set, Avi Shinnar
- Re: [Coq-Club] going from equality in Type to equality in Set, muad