Hi all,<br><br>Adding one thing:<br><br><div class="gmail_quote">2011/8/31 José Pedro Magalhães <span dir="ltr">&lt;<a href="mailto:jpm@cs.uu.nl">jpm@cs.uu.nl</a>&gt;</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&#39;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&#39;ve just shown that âŸ¦ C âŸ§â‚ â‰¡ âŸ¦ U₁→Uâ‚‚ C âŸ§â‚‚.<br><br><br>Thanks,<br>Pedro<br>