Casting from a to b then b to a is identity?

user_5339728 0
Viewed 50

Given the definition:

Definition cast (a b:Type) (p:a = b) (x:a) : b :=
    match p with
    | eq_refl _  => x
    end.

I was hoping that the following lemma would be provable:

Lemma cast_cast_is_id : forall (a b:Type) (x:a) (p:a = b) (q:b = a),
    cast b a q (cast a b p x) = x.

However, I do not seem to be able to carry out a proof for this. I can destruct p successfully, but cannot destruct q after that. Replacing the lemma's statement with eq_sym p instead of arbitrary q does not help me either it seems.

I fear I have unwittingly stumbled into some subtle point of HoTT.

Can anyone prove this lemma or is it known to be unprovable without further axioms?

coq
1 Answers

I am not completely sure, but it seems to me that what you are trying to prove is no different from forall a (p:a=a), p = eq_refl. If so, you cannot prove it in Coq, unless you know something about a, e.g., decidable equality. In that case, you can use the results on UIP (unicity of identity proofs) from the standard library.

user_134991210
Related