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

[Abhishek Anand]

It is known that UIP is inconsistent with univalence.
Does this typecheck even after disabling UIP(==K axiom?) ?
I might be wrong, but I think that UIP is baked into the typechecker of
Agda.
But, UIP can be disabled somehow?


-- Abhishek
http://www.cs.cornell.edu/~aa755/


On Mon, Jan 6, 2014 at 3:42 PM, Maxime Dénès <mail at maximedenes.fr> wrote:

> 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
>>
>
> _______________________________________________
> 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/20140106/129d38e2/attachment-0001.html