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

[Maxime Dénès]

Well, my example does not typecheck with the --without-K flag.

However, the same thing can be proven in Coq without K, so I am not sure 
if it is because the flag is too restrictive or because Agda's pattern 
matching is different.

I am also not sure how specific the problem is to univalence. As Cody 
said, I would expect to find some set-theoretical models where the 
equality holds. So being able to prove the negation is disturbing.

Maxime.

On 01/06/2014 07:23 PM, Abhishek Anand wrote:
> 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/ <http://www.cs.cornell.edu/%7Eaa755/>
>
>
> On Mon, Jan 6, 2014 at 3:42 PM, Maxime Dénès <mail at maximedenes.fr 
> <mailto: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
>             <mailto: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 <mailto:Agda at lists.chalmers.se>
>         https://lists.chalmers.se/mailman/listinfo/agda
>
>
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>