[Agda] Re: Problem with propositional equality (or my understanding of it)

[Ulf Norell]

2011/8/31 José Pedro Magalhães <jpm at cs.uu.nl>

> Hi all,
>
> \begin{code}
>>   prop : (C : U₁) → (x : ⟦ C ⟧₁) → ⟦⟧₁→⟦⟧₂ C (id₁ C x) ≡ ⟦⟧₁→⟦⟧₂ C x
>>   prop Z₁     tt       = refl
>>   prop (S₁ x) (just y) = cong {!just!} (prop x y)
>>   prop (S₁ x) nothing  = refl
>> \end{code}
>>
>
You can prove prop by first showing that id₁ is the identity in U₁ and then
lift the proof to U₂ as follows:

  lem : (C : U₁) → (x : ⟦ C ⟧₁) → id₁ C x ≡ x
  lem Z₁     tt       = refl
  lem (S₁ C) (just x) = cong just (lem C x)
  lem (S₁ C) nothing  = refl

  prop : (C : U₁) → (x : ⟦ C ⟧₁) → ⟦⟧₁→⟦⟧₂ C (id₁ C x) ≡ ⟦⟧₁→⟦⟧₂ C x
  prop C x = cong (⟦⟧₁→⟦⟧₂ C) (lem C x)

The reason cong just doesn't work in your version is that ≡→ can only
make progress if its argument is refl, and that only happens for ⟦⟧₁≡⟦⟧₂ C
when C is completely known. Matching on the top-level of C doesn't reveal
more structure in the equality proof (unlike in SecondTry).

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110831/fb88beca/attachment.html