The Coq mailing list

[Cody Roux <cody.roux AT andrew.cmu.edu>]

Of course, prop_ext in inconsistent with the current version of Coq, so this proof shouldn't come as a surprise... :)



On 01/28/2014 04:51 PM, Jason Gross wrote:

You don't even need bracket types if you have prop_ext:

Axiom prop_ext: forall (p q : Prop), (p <-> q) -> p = q.

Goal forall (a b : Prop), @eq Type a b -> @eq Prop a b.

Proof.

  intros a b H.

  apply prop_ext.

  split; destruct H; apply id.

Defined.

On Tue, Jan 28, 2014 at 4:45 PM, Jeremy Avigad <avigad AT cmu.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.

Good point. Here is how to do it using propositional extensionality.

(Sorry for the lousy proof scripts. I have been away from Coq for a while.)

Best wishes,

Jeremy

**********************

Axiom prop_ext: forall (p q : Prop), (p <-> q) -> p = q.

Section Test.

Variables a b : Prop.
Variable p : @eq Type a b.

Definition bracket (A : Type) : Prop := forall (P : Prop), (A -> P) -> P.

Lemma bracket_eq (x : Prop): bracket x = x.
  apply prop_ext.
  split.
  intro H.
    apply (H x).
    intro H1. apply H1.
  intros H P H1.
  apply (H1 H).
Qed.
 
Lemma coerce: @eq Prop a b.
  transitivity (bracket a).
    symmetry. apply bracket_eq.
  transitivity (bracket b).
    rewrite p. reflexivity.
  apply bracket_eq.
Qed.

End Test.

On 01/28/2014 03:50 PM, Vladimir Voevodsky 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