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

[Aaron Stump]

Related (I hope) to the discussion of eliminators, I want to point out 
that if we were working in a type theory based on positive recursive 
types rather than primitive datatypes, this example would not go through 
(of course).

Empty := mu X.X

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

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).

Cheers,
Aaron

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140108/2a493ed5/attachment.html