[Agda] Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

[Maxime Dénès]

Bingo, Agda seems to have the same problem:

module Termination where

open import Relation.Binary.Core

data Empty : Set where

data Box : Set where
wrap : (Empty → Box) → Box

postulate
iso : (Empty → Box) ≡ Box

loop : Box -> Empty
loop (wrap x) rewrite iso = loop x

gift : Empty → Box
gift ()

bug : Empty
bug = loop (wrap gift)

However, I may be missing something due to my ignorance of Agda. It may 
be well known that the axiom I introduced is inconsistent. Forgive me if 
it is the case.

Maxime.

On 01/06/2014 01:15 PM, Maxime Dénès wrote:
> The anti-extensionality bug is indeed related to termination. More 
> precisely, it is the subterm relation used by the guard checker which 
> is not defined quite the right way on dependent pattern matching.
>
> It is not too hard to fix (we have a patch), but doing so without 
> ruling out any interesting legitimate example (dealing with recursion 
> on dependently typed data structures) is more challenging.
>
> I am also curious as to whether Agda is impacted. Let's try it :)
>
> Maxime.
>
> On 01/06/2014 12:59 PM, Altenkirch Thorsten wrote:
>> Which bug was this?
>>
>> I only saw the one which allowed you to prove anti-extensionality? But
>> this wasn't related to termination, or?
>>
>> Thorsten
>>
>> On 06/01/2014 16:54, "Cody Roux" <cody.roux at andrew.cmu.edu> wrote:
>>
>>> Nice summary!
>>>
>>>
>>> On 01/06/2014 08:49 AM, Altenkirch Thorsten wrote:
>>>> Agda enforces termination via a termination checker which is more
>>>> flexible but I think less principled than Coq's approach.
>>> That's a bit scary given that there was an inconsistency found in
>>> the Coq termination checker just a couple of weeks ago :)
>>>
>>> BTW, has anyone tried reproducing the bug in Agda?
>>>
>>>
>>> Cody
>> This message and any attachment are intended solely for the addressee 
>> and may contain confidential information. If you have received this 
>> message in error, please send it back to me, and immediately delete 
>> it. Please do not use, copy or disclose the information contained in 
>> this message or in any attachment. Any views or opinions expressed by 
>> the author of this email do not necessarily reflect the views of the 
>> University of Nottingham.
>>
>> This message has been checked for viruses but the contents of an 
>> attachment
>> may still contain software viruses which could damage your computer 
>> system, you are advised to perform your own checks. Email 
>> communications with the University of Nottingham may be monitored as 
>> permitted by UK legislation.
>>
>>
>>
>>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda