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

Conor McBride conor at strictlypositive.org
Tue Jan 7 17:42:37 CET 2014


On 7 Jan 2014, at 09:28, Altenkirch Thorsten =
<psztxa at exmail.nottingham.ac.uk> wrote:

>=20
>=20
> On 07/01/2014 00:50, "Maxime D=A8=A6n=A8=A8s" <mail at maximedenes.fr> =
wrote:
>=20
>> Well, my example does not typecheck with the --without-K flag.
>>=20
>> 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.
>=20
> Very good. Agda is right and Coq got it wrong. As I said previosuly =
the
> definition of loop implicitely uses K.

Not so fast! The code below is accepted using the --without-K flag, and
the elimination that noo does is a based path induction, IIUC.

Conor

{-# OPTIONS --without-K #-}

module BadWithoutK where

data Zero : Set where

data WOne : Set where
  wrap : (Zero -> WOne) -> WOne

data _<->_ (X : Set) : Set -> Set where
  Refl : X <-> X

postulate
  myIso : WOne <-> (Zero -> WOne)

moo : WOne -> Zero
noo : (X : Set) -> (WOne <-> X) -> X -> Zero

moo (wrap f) =3D noo (Zero -> WOne) myIso f
noo .WOne Refl x =3D moo x

bad : Zero
bad =3D moo (wrap \ ())



>=20
> T.
>=20
>>=20
>> 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.
>>=20
>> Maxime.
>>=20
>> 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(=3D=3DK axiom?) ?
>>> I might be wrong, but I think that UIP is baked into the typechecker
>>> of Agda.
>>> But, UIP can be disabled somehow?
>>>=20
>>>=20
>>> -- Abhishek
>>> http://www.cs.cornell.edu/~aa755/ =
<http://www.cs.cornell.edu/%7Eaa755/>
>>>=20
>>>=20
>>> On Mon, Jan 6, 2014 at 3:42 PM, Maxime D=A8=A6n=A8=A8s =
<mail at maximedenes.fr
>>> <mailto:mail at maximedenes.fr>> wrote:
>>>=20
>>>    Bingo, Agda seems to have the same problem:
>>>=20
>>>    module Termination where
>>>=20
>>>    open import Relation.Binary.Core
>>>=20
>>>    data Empty : Set where
>>>=20
>>>    data Box : Set where
>>>    wrap : (Empty =A1=FA Box) =A1=FA Box
>>>=20
>>>    postulate
>>>    iso : (Empty =A1=FA Box) =A1=D4 Box
>>>=20
>>>    loop : Box -> Empty
>>>    loop (wrap x) rewrite iso =3D loop x
>>>=20
>>>    gift : Empty =A1=FA Box
>>>    gift ()
>>>=20
>>>    bug : Empty
>>>    bug =3D loop (wrap gift)
>>>=20
>>>    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.
>>>=20
>>>    Maxime.
>>>=20
>>>=20
>>>    On 01/06/2014 01:15 PM, Maxime D=A8=A6n=A8=A8s wrote:
>>>=20
>>>        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.
>>>=20
>>>        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.
>>>=20
>>>        I am also curious as to whether Agda is impacted. Let's try =
it
>>> :)
>>>=20
>>>        Maxime.
>>>=20
>>>        On 01/06/2014 12:59 PM, Altenkirch Thorsten wrote:
>>>=20
>>>            Which bug was this?
>>>=20
>>>            I only saw the one which allowed you to prove
>>>            anti-extensionality? But
>>>            this wasn't related to termination, or?
>>>=20
>>>            Thorsten
>>>=20
>>>            On 06/01/2014 16:54, "Cody Roux" =
<cody.roux at andrew.cmu.edu
>>>            <mailto:cody.roux at andrew.cmu.edu>> wrote:
>>>=20
>>>                Nice summary!
>>>=20
>>>=20
>>>                On 01/06/2014 08:49 AM, Altenkirch Thorsten wrote:
>>>=20
>>>                    Agda enforces termination via a termination
>>>                    checker which is more
>>>                    flexible but I think less principled than Coq's
>>>                    approach.
>>>=20
>>>                That's a bit scary given that there was an
>>>                inconsistency found in
>>>                the Coq termination checker just a couple of weeks =
ago
>>> :)
>>>=20
>>>                BTW, has anyone tried reproducing the bug in Agda?
>>>=20
>>>=20
>>>                Cody
>>>=20
>>>            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.
>>>=20
>>>            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.
>>>=20
>>>=20
>>>=20
>>>=20
>>>=20
>>>        _______________________________________________
>>>        Agda mailing list
>>>        Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>>        https://lists.chalmers.se/mailman/listinfo/agda
>>>=20
>>>=20
>>>    _______________________________________________
>>>    Agda mailing list
>>>    Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>>    https://lists.chalmers.se/mailman/listinfo/agda
>>>=20
>>>=20
>>=20
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>=20
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda



More information about the Agda mailing list