The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

That's done in this paper:
http://arxiv.org/abs/1309.5767

On Tue, Jan 28, 2014 at 11:32 PM, Vladimir Voevodsky 
<vladimir AT ias.edu>
 wrote:
> There is another way to define bracket in Coq. Something like that:
>
> Inductive bracket ( A : Type ) : Prop := wit : A -> bracket A .
>
> V.
>
>
>
>
>
>
>
> On 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
>>
>>
>
>
>
>