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

[Vladimir Voevodsky]

In my opinion only those constructions which can be expressed through eliminators are trustworthy. There is really no other way to supply rigorousness to inductive types with  pseudo-parameters (or whatever they are now called) such as Id-types.

V.


On Jan 6, 2014, at 6:27 PM, Cody Roux <cody.roux at andrew.cmu.edu> wrote:

> The thing about Coq is that it's very disturbing not to have a
> Set-theoretic interpretation where Prop is the set of Booleans {True,
> False}. Agda of course doesn't have these qualms, but the fact that this
> issue appears in Coq without use of anything fancy (impredicativity,
> etc) makes me still a bit worried. In particular there should be a
> Set-theoretic model for Agda where Empty -> Box and Box -are- equal:
> with a sufficiently clever interpretation of inductives, I believe I can
> get [[Empty -> Box ]] = [[Box]] = { {} } (where {} is just the empty
> set). Can someone with more Agda knowledge try to type the original
> problematic term?
> 
> 
> Hypothesis Heq : (False -> False) = True.
> 
> Fixpoint contradiction (u : True) : False :=
> contradiction (
> match Heq in (_ = T) return T with
> | eq_refl => fun f:False => match f with end
> end
> ).
> 
> 
> 
> On 01/06/2014 06:12 PM, Altenkirch Thorsten wrote:
>> Hi Maxime,
>> 
>> your postulate seems correct since certainly Empty → Box and Box are
>> isomorphic and hence equal as a consequence of univalence.
>> 
>> However, I think the definition of loop looks suspicious in the presence
>> of proof-relevant equality: if we replace rewrite by an explicit use of
>> subst, loop isn't structural recursive anymore. Hence my diagnosis would
>> be that rewrite is simply incompatible with univalence.
>> 
>> Cheers,
>> Thorsten
>> 
>> On 06/01/2014 20:42, "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
>