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

[Andreas Abel]

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?

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?

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
>