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

[Andrea Vezzosi]

It might make sense to state and prove f with heterogeneous equality
instead, it's possibly a weaker statement, but you won't have subst in
the type then.



On Wed, May 3, 2017 at 10:58 AM, Apostolis Xekoukoulotakis
<apostolis.xekoukoulotakis at gmail.com> wrote:
> 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
>>>
>>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>