[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy
theory & advantage of UF/Coq
Andreas Abel
andreas.abel at ifi.lmu.de
Wed Jan 8 18:53:56 CET 2014
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 \ ())
--
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/
-------------- next part --------------
{-# OPTIONS --without-K #-}
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 \ ())
More information about the Agda
mailing list