The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

It should be possible to do using the "bracket type" projection Type -> Prop  but I am not sure how exactly it works in Coq since I do not use Prop.

V.

On Jan 28, 2014, at 2:30 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

There is no way without axioms.  Going the other way is straightforwad: "match (H : @eq Prop x y) in (_ = y') return (@eq Type x y') with eq_refl => eq_refl end".  It does not work going the other way because y' would be a Type, and you'd be trying to make it a Prop.  If you think about this homotopy-theoretically (google homotopy type theory), there is no guarantee that every point along a path @eq Type_i (x : Type_j) (y : Type_j) will be small enough to fit into a Type_j.  You could do it with Axiom K, I believe.

-Jason

On Jan 28, 2014 1:06 PM, "Leonardo de Moura" <leonardo AT microsoft.com> wrote:

Hi,

 

Given (x y : Prop), I’m wondering about how to coerce an equality proof for (@eq Type x y) to (@eq Prop x y).

Is this possible?

 

Thanks,

Leo