[Agda] Help at propositional equality proof that contains subst.

[Jesper Cockx]

Hi,

Did you already try to use `with (eq a)` and then match with refl? I think
that should do the trick.

Otherwise, the brute-force way to get rid of annoying equality proofs in
your types is by using the J eliminator. But the result is usually not very
pretty...

-- Jesper

On Wed, May 3, 2017 at 9:24 AM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> Hello,
>
> I have something like this :
>
> ```
> postulate
>   B : Set
>   A : B → Set
>   big_expression : {b : B} → (a : A b) → B
>   h : {b : B} → (a : A b) → A (big_expression a)
>   eq : {b : B} → (a : A b) → (big_expression a) ≡ b
>
> f : {b : B} → (a : A b) → subst A (eq a) (h a) ≡ a
> f = {!!}
>
> ```
>
> h is defined inductively, thus it would be very easy to prove this if I
> did not have subst in the equality.
>
> Any advice on how to proceed?
>
> I can't find a way to remove subst.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170503/644cd415/attachment.html>