The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tue, Jun 26, 2012 at 8:49 PM, Jason Gross 
<jasongross9 AT gmail.com>
 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?

Well, if you assume a projection operator from Type to Set, you can prove 
it...

Parameter Type_Set_proj : Type -> Set.
Axiom Type_Set_proj_is_proj : forall a:Set,
  @eq Set (Type_Set_proj a) a.

Lemma eqType2Set (a b : Set) : @eq Type a b -> @eq Set a b.
Proof.
assert (forall (a':Set) (b':Type),
  @eq Type a' b' -> @eq Set a' (Type_Set_proj b')).
destruct 1.
symmetry; apply Type_Set_proj_is_proj.
intros.
rewrite <- (Type_Set_proj_is_proj b).
apply H.
exact H0.
Qed.

Given that a match statement on e : @eq Type a b would look something like
match e in (@eq Type _ b') return (f b') with
| eq_refl => ...
end
where b' is a general element of Type, you probably need something
similar to such a projection.

I also suspect such a projection is probably consistent -- on a meta
level, you should be able to look at the definition of the Type
argument, see if it fits into Set, and if so return the coercion into
Set; and otherwise, return unit.
-- 
Daniel Schepler