[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