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

[Cody Roux]

On 01/07/2014 04:19 AM, Altenkirch Thorsten wrote:
> A convincing way to justify those systems would be to provide a
> translation into eliminators. I suggested this to Andreas a while ago. 

That sounds fair. A couple years ago, I tried seeing if there was a
straightforward way to perform this translation (with Jorge Sacchini).
It's not trivial, and in particular I found that I would probably need
some form of proof-irrelevance, even for "first-order" datatypes, which
seems ironic. However in this case we would only need it on "h-level 0"
so it doesn't seem hopeless.

Higher-order datatypes are a bit more difficult, and I admit I never
worked it out. I believe it's possible though.

>> The fact that the implementation is behind the theoretical capabilities
>> is just that, an implementation problem.
> The eliminators are like axioms in set theory and it is worthwhile to
> translate any extension by reducing them to the axiom instead of adding
> new ones even though they may be semantically justified.
That's fair, but I don't see why eliminators have a more powerful
ontological status than sized-types. They require work to be derived as
well, and the correctness proofs for them are quite similar to that for
sized types. This seems like a matter of preference. Obviously I'm not
neutral in this matter though.

Best,

Cody



> Thorsten
>
>
>> 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