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

[José Pedro Magalhães]

Hi all,

Adding one thing:

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

>
> \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}
>
>
In the problematic branch, if I try to first match on the evidence:
\begin{code}
  prop (S₁ x) (just y) with (cong Maybe (⟦⟧₁≡⟦⟧₂ x))
  prop (S₁ x) (just y) | refl = ?
\end{code}

I get

⟦ x ⟧₁ != ⟦ U₁→U₂ x ⟧₂ of type Set
> when checking that the pattern refl has type
> Maybe ⟦ x ⟧₁ ≡ Maybe ⟦ U₁→U₂ x ⟧₂
>

I'm not entirely sure how to interpret this...

What I am trying to understand is if there is a way to keep my proofs short
like in FirstTry.
Also, it feels a bit dumb to have to explicitly spell out how to go from ⟦ C
⟧₁ → ⟦ U₁→U₂ C ⟧₂,
when I've just shown that ⟦ C ⟧₁ ≡ ⟦ U₁→U₂ C ⟧₂.


Thanks,
Pedro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110831/16e360bc/attachment.html