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

[Cody Roux]

On 01/06/2014 06:36 PM, Vladimir Voevodsky wrote:
> 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.
This is simply not true, there are whole PhDs dedicated to describing 
systems which can do better than eliminators. Andreas mentioned 
sized-types, which are IMO the most mature candidate.

The fact that the implementation is behind the theoretical capabilities 
is just that, an implementation problem.

Best,

Cody


> 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