The Coq mailing list

[muad <muad.dib.space AT gmail.com>]

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.
-- 
View this message in context: 
http://www.nabble.com/going-from-equality-in-Type-to-equality-in-Set-tp25665030p25669211.html
Sent from the Coq mailing list archive at Nabble.com.