going from equality in Type to equality in Set

[Avi Shinnar]

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

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[muad]

Avi Shinnar wrote:

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

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

I don't believe it to be possible because Set is a subtype of Type. That is Type is more general, the converse (eq in Set to eq in Type) is possible though.