<br><div class="gmail_quote">2011/8/31 José Pedro Magalhães <span dir="ltr"><<a href="mailto:jpm@cs.uu.nl">jpm@cs.uu.nl</a>></span><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hi all,<br><br><div class="im"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
\begin{code}<br>
prop : (C : U₁) → (x : ⟦ C ⟧₁) → ⟦⟧₁→⟦⟧₂ C (id₁ C x) ≡ ⟦⟧₁→⟦⟧₂ C x<br>
prop Z₁ tt = refl<br>
prop (S₁ x) (just y) = cong {!just!} (prop x y)<br>
prop (S₁ x) nothing = refl<br>
\end{code}<br></blockquote></div></div></blockquote><div><br></div><div>You can prove prop by first showing that id₁ is the identity in U₁ and then</div><div>lift the proof to U₂ as follows:</div><div><br></div><div> lem : (C : U₁) → (x : ⟦ C ⟧₁) → id₁ C x ≡ x</div>
<div> lem Z₁ tt = refl</div><div> lem (S₁ C) (just x) = cong just (lem C x)</div><div> lem (S₁ C) nothing = refl</div><div><br></div><div> prop : (C : U₁) → (x : ⟦ C ⟧₁) → ⟦⟧₁→⟦⟧₂ C (id₁ C x) ≡ ⟦⟧₁→⟦⟧₂ C x</div>
<div> prop C x = cong (⟦⟧₁→⟦⟧₂ C) (lem C x)</div><div> </div><div>The reason cong just doesn't work in your version is that ≡→ can only</div><div>make progress if its argument is refl, and that only happens for ⟦⟧₁≡⟦⟧₂ C</div>
<div>when C is completely known. Matching on the top-level of C doesn't reveal</div><div>more structure in the equality proof (unlike in SecondTry).</div><div><br></div><div>/ Ulf</div></div>