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

[Jesper Cockx]

I tried to find a solution, but I think what you're trying to do is
impossible. You have postulated a proof of `(big_expression a) ≡ b`, but an
actual proof of this equality is impossible because this would imply that
`a` has type `A (big_expression a)`, which is cyclic. The unifier
(sensibly) refuses to construct this cyclic type of `a`, so matching with
refl on the proof fails. Since it's impossible to have this proof reduce to
`refl`, it's also impossible to simplify the expression `subst A (eq a) (h
a)`.

-- Jesper

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
>>>
>>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170503/dad1289c/attachment.html>