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

[Apostolis Xekoukoulotakis]

I tried 'with (big_expression a) | (eq a)' . It does not work because of
the h function.

It says that the result is not well typed.

>From what I understand, we cannot abstract (eq a) without abstracting the h
function, but I need the h function to do the proof.



On Wed, May 3, 2017 at 11:51 AM, Jesper Cockx <Jesper at sikanda.be> wrote:

> 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/dcd74131/attachment.html>