The Coq mailing list

[Voevodsky <vladimir AT ias.edu>]

I am not sure that such a map can be constructed in Coq. There is no particular reason why the Id type in the larger universe should map to the Id type in the smaller universe.

Vladimir.




On 6/26/12 11:49 PM, Jason Gross wrote:

I'm trying to prove the following lemma, and getting an error on [Qed].

Lemma eqType2Set (a b : Set) : @eq Type a b -> @eq Set a b.

  intro; subst; reflexivity.

Qed.

Coq says

Error: Illegal application (Type Error): 

The term "eq" of type "forall A : Type, A -> A -> Prop"

cannot be applied to the terms

 "Set" : "Type"

 "a0" : "Type"

 "b" : "Set"

The 2nd term has type "Type" which should be coercible to 

"Set".

If I [Set Printing All] and [Show Proof], Coq tells me that the proof is 

(fun (a b : Set) (H : @eq Type a b) =>

 @eq_ind_r Type b (fun a0 : Type => @eq Set a0 b) (@eq_refl Set b) a H)

Does anyone have ideas/suggestions for how to make this proof go through?  Does it need an axiom?

-Jason