Hi all,<br><br>Adding one thing:<br><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;">
<br>
\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>
<br></blockquote></div><br>In the problematic branch, if I try to first match on the evidence:<br>\begin{code}<br> prop (S₁ x) (just y) with (cong Maybe (⟦⟧₁≡⟦⟧₂ x))<br> prop (S₁ x) (just y) | refl = ?<br>\end{code}<br>
<br>I get<br><br><blockquote style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;" class="gmail_quote">⟦ x ⟧₁ != ⟦ U₁→U₂ x ⟧₂ of type Set<br>when checking that the pattern refl has type<br>
Maybe ⟦ x ⟧₁ ≡ Maybe ⟦ U₁→U₂ x ⟧₂<br></blockquote><br>I'm not entirely sure how to interpret this...<br><br>What I am trying to understand is if there is a way to keep my proofs short like in FirstTry.<br>Also, it feels a bit dumb to have to explicitly spell out how to go from ⟦ C ⟧₁ → ⟦ U₁→U₂ C ⟧₂,<br>
when I've just shown that ⟦ C ⟧₁ ≡ ⟦ U₁→U₂ C ⟧₂.<br><br><br>Thanks,<br>Pedro<br>