<div dir="ltr"><div><div><div>I think that I introduced the cycle in my attempt to simplify the example.<br><br></div>This seems to be closer to what my code actually looks like:<br><br>```<br><br>postulate<br>  B : Set<br>  A : B → Set<br>  big_expression : (c : B) → {b : B} → (a : A b) → B<br>  h : (c : B) → {b : B} → (a : A b) → A (big_expression c a)<br>  eq : (c : B) → {b : B} → (a : A b) → (big_expression c a) ≡ c<br><br>f : {b : B} → (a : A b) → subst A (eq b a) (h b a) ≡ a<br>f = {!!}<br><br><br>```<br><br></div>I hope that this is cycle free.<br><br></div>(In my code eq holds under stricter conditions than h`s input but here their inputs are the same. f is to be proved under these stricter conditions.)<br><div><div><br></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, May 3, 2017 at 5:47 PM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div>I uploaded my code to see the actual function.<br><a href="https://github.com/xekoukou/sparrow/blob/750bcebeb488c52f1b95083e8cff79f5032125a1/agda/IndexLLProp.agda#L178" target="_blank"><br>https://github.com/xekoukou/<wbr>sparrow/blob/<wbr>750bcebeb488c52f1b95083e8cff79<wbr>f5032125a1/agda/IndexLLProp.<wbr>agda#L178</a><br><br></div>The proofs I use in 'subst2' are here:<br><br><a href="https://github.com/xekoukou/sparrow/blob/750bcebeb488c52f1b95083e8cff79f5032125a1/agda/IndexLLProp.agda#L154" target="_blank">https://github.com/xekoukou/<wbr>sparrow/blob/<wbr>750bcebeb488c52f1b95083e8cff79<wbr>f5032125a1/agda/IndexLLProp.<wbr>agda#L154</a><br><br><a href="https://github.com/xekoukou/sparrow/blob/750bcebeb488c52f1b95083e8cff79f5032125a1/agda/LinLogic.agda#L135" target="_blank">https://github.com/xekoukou/<wbr>sparrow/blob/<wbr>750bcebeb488c52f1b95083e8cff79<wbr>f5032125a1/agda/LinLogic.agda#<wbr>L135</a><br><br></div>Andrea, <br></div>  I tried to use heterogeneous equality. I will give it one more try.<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Wed, May 3, 2017 at 3:12 PM, Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">It might make sense to state and prove f with heterogeneous equality<br>
instead, it's possibly a weaker statement, but you won't have subst in<br>
the type then.<br>
<br>
<br>
<br>
On Wed, May 3, 2017 at 10:58 AM, Apostolis Xekoukoulotakis<br>
<div class="m_-5635430848420327611HOEnZb"><div class="m_-5635430848420327611h5"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gma<wbr>il.com</a>> wrote:<br>
> I tried 'with (big_expression a) | (eq a)' . It does not work because of the<br>
> h function.<br>
><br>
> It says that the result is not well typed.<br>
><br>
> From what I understand, we cannot abstract (eq a) without abstracting the h<br>
> function, but I need the h function to do the proof.<br>
><br>
><br>
><br>
> On Wed, May 3, 2017 at 11:51 AM, Jesper Cockx <<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>> wrote:<br>
>><br>
>> Hi,<br>
>><br>
>> Did you already try to use `with (eq a)` and then match with refl? I think<br>
>> that should do the trick.<br>
>><br>
>> Otherwise, the brute-force way to get rid of annoying equality proofs in<br>
>> your types is by using the J eliminator. But the result is usually not very<br>
>> pretty...<br>
>><br>
>> -- Jesper<br>
>><br>
>> On Wed, May 3, 2017 at 9:24 AM, Apostolis Xekoukoulotakis<br>
>> <<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gma<wbr>il.com</a>> wrote:<br>
>>><br>
>>> Hello,<br>
>>><br>
>>> I have something like this :<br>
>>><br>
>>> ```<br>
>>> postulate<br>
>>>   B : Set<br>
>>>   A : B → Set<br>
>>>   big_expression : {b : B} → (a : A b) → B<br>
>>>   h : {b : B} → (a : A b) → A (big_expression a)<br>
>>>   eq : {b : B} → (a : A b) → (big_expression a) ≡ b<br>
>>><br>
>>> f : {b : B} → (a : A b) → subst A (eq a) (h a) ≡ a<br>
>>> f = {!!}<br>
>>><br>
>>> ```<br>
>>><br>
>>> h is defined inductively, thus it would be very easy to prove this if I<br>
>>> did not have subst in the equality.<br>
>>><br>
>>> Any advice on how to proceed?<br>
>>><br>
>>> I can't find a way to remove subst.<br>
>>><br>
>>> ______________________________<wbr>_________________<br>
>>> Agda mailing list<br>
>>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
>>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
>>><br>
>><br>
><br>
><br>
> ______________________________<wbr>_________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
><br>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>