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

[Aaron Stump]

Hi, Andreas.

On 01/08/2014 12:46 PM, Andreas Abel wrote:
> On 08.01.14 7:37 PM, Aaron Stump wrote:
>> Box := mu X. (Empty -> X)
>>
>> Note that X occurs positively in the body of the mu-type for Box. The
>> theory gives us a recursor R with this typing rule
>>
>> b : Box
>> f : (Empty -> T) -> T
>> ---------------------
>> R(b,f) : T
>
> Mmh, why is this the recursor?  Should not T depend on (b : Box) or 
> something similar?

Sorry, you are right: this is the iterator, of course.

>
> This looks like the iterator to me...  Maybe that's what you meant...
>
>> We certainly have the isomorphism Box = (Empty -> Box) -- it is even a
>> definitional equality! -- but we cannot use this recursor to write a
>> term of type Box -> Empty.  The best we could do would be to start like
>> this, where g has type Empty -> Empty, and hence is useless for deriving
>> Empty.
>>
>> loop = \ b . R(b, \ g . (g ?))
>>
>> So I think the wrap constructor being used in Maxime's code is just an
>> explicit witness of the above implicit isomorphism.  Removing it should
>> not count for structural decrease (obviously).
>
> Where would you locate the structural decrease instead?
I do not have a proposal for how to address the problem in Agda, since I 
do not know the exact formal system behind Agda well enough to comment.  
I just wanted to connect this problem with a simpler type theory, in 
case it sheds light on the more complex situation here.

Aaron

>
> Cheers,
> Andreas
>
>> On 01/08/2014 11:53 AM, Andreas Abel wrote:
>>> Conor,
>>>
>>> that's on the latest darcs version of Agda, I guess?
>>>
>>> At least my own version of --without-K rejects your match on Refl:
>>>
>>> The indices
>>>    WOne
>>>    X
>>> are not constructors (or literals) applied to variables (note that
>>> parameters count as constructor arguments)
>>> when checking that the pattern Refl has type WOne <-> X
>>>
>>> But you say it is justified, is it?
>>>
>>> Cheers,
>>> Andreas
>>>
>>> On 07.01.2014 17:42, Conor McBride wrote:
>>>>> 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) = noo (Zero -> WOne) myIso f
>>>> noo .WOne Refl x = moo x
>>>>
>>>> bad : Zero
>>>> bad = moo (wrap \ ())
>>>
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>