The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You can get [@eq Prop (inhabited x) (inhabited y)], which is [@eq Prop ||x|| ||y||].  But this still does not give you [@eq Prop x y] without axioms, because there's no theorem that [inhabited : Type -> Prop] is injective on Props.  With univalence, though, you could do it.

-Jason

On Tue, Jan 28, 2014 at 3:50 PM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

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