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

[Altenkirch Thorsten]

It would be good if without-K rejects this.

I think that the problem is related to proof-irrelevance, namely if we
believe that the only constructor of equality is refl it is clear that
subst should preserve the structural ordering.

However, it is not clear to me that the syntactic check for without-K
would fix this problem. In particular since this particular construction
isn't derivable using the eliminator K either.

On 08/01/2014 17:53, "Andreas Abel" <andreas.abel at ifi.lmu.de> 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?

What do you mean by this?

I haven't reread Conor's paper or PhD but from what he says it seems that
this was a bug. This happens to the best - hence it would be really a good
idea if our pattern schemes can be justified by a formal and
machine-checkable evidence.

Thorsten

P.S. In our old foetus paper we also define an untyped structural ordering
on terms.


>
>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 \ ())
>
>-- 
>Andreas Abel  <><      Du bist der geliebte Mensch.
>
>Theoretical Computer Science, University of Munich
>Oettingenstr. 67, D-80538 Munich, GERMANY
>
>andreas.abel at ifi.lmu.de
>http://www2.tcs.ifi.lmu.de/~abel/

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.