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

[Andreas Abel]

Conor,

The small problem is that your translation below has holes that cannot
be filled. ;-)

Thus, since your code using pattern matching cannot be translated into
eliminators, it should be rejected by a test that ensures this.

Maybe my version of --without-K is such a test.  A patch is on

  http://code.google.com/p/agda/issues/detail?id=1023

One difference to the current official version of --without-K is that it
treats parameters that are used "non-linearly" in a constructor are
treated as indices, not as parameters.  This means that there is no
difference between

  data _<->_ (X : Set) : Set -> Set1 where refl : X <-> X

and

  data _<->_ : Set -> Set -> Set1 where refl : {X : Set} -> X <-> X.

As a consequence, equality is treated symmetrically.  Thus, it does not
matter whether you write

  WOne <-> X    or     X <-> WOne

meaning you cannot cheat your way around the test by putting the bad
stuff (WOne) in the parameter and the good stuff (X) in the index, as
you can do with the current version.

Cheers,
Andreas

On 09.01.14 12:10 PM, Conor McBride wrote:
> 
> On 8 Jan 2014, at 17:53, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> 
>> Conor,
>>
>> that's on the latest darcs version of Agda, I guess?
> 
> No. 2.3.2.1 from cabal.
> 
>>
>> 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?
> 
> I believe so.
> 
> This is quite like the thing Jesper wrote yesterday, but with labelled
> types, built as records, for added clarity. At each step, I show the
> labelled type of the programming problem, corresponding to the left-hand
> side of the function being constructed. The pattern refinement of Noo
> is exactly that given by the standard-issue eliminator for <->.
> 
> Note that I've used only case analysis here, the purpose being to show
> that the covering can be constructed without K.
> 
> Cheers
> 
> Conor
> 
> ---
> {-# OPTIONS --without-K #-}
> 
> module PE where
> 
> data Zero : Set where
> 
> elimZero : (z : Zero)(P : Zero -> Set) -> P z
> elimZero ()
> 
> data WOne : Set where
>    wrap : (Zero -> WOne) -> WOne
> 
> elimWOne : (x : WOne) ->
>    (P : WOne -> Set) ->
>    ((f : Zero -> WOne) -> ((z : Zero) -> P (f z)) -> P (wrap f)) ->
>    P x
> elimWOne (wrap f) P p = p f \ z -> elimWOne (f z) P p
> 
> caseWOne : (x : WOne) ->
>    (P : WOne -> Set) ->
>    ((f : Zero -> WOne) -> P (wrap f)) ->
>    P x
> caseWOne w P p = elimWOne w P \ f _ -> p f
> 
> data _<->_ (X : Set) : Set -> Set where
>    Refl : X <-> X
> 
> elim<-> : {X Y : Set}(Q : X <-> Y) ->
>    (P : (Y : Set)(Q : X <-> Y) -> Set) ->
>    P X Refl ->
>    P Y Q
> elim<-> Refl P p = p
> 
> postulate
>    myIso : WOne <-> (Zero -> WOne)
> 
> record Moo (w : WOne) : Set where
>    constructor moo=
>    field
>      callMoo : Zero
> open Moo
> 
> moo' : (w : WOne) -> Moo w -> Zero
> moo' w = callMoo
> 
> record Noo (X : Set)(Q : WOne <-> X)(x : X) : Set where
>    constructor noo=
>    field
>      callNoo : Zero
> open Noo
> 
> noo' : (X : Set)(Q : WOne <-> X)(x : X) -> Noo X Q x -> Zero
> noo' X Q x = callNoo
> 
> noo : (X : Set)(Q : WOne <-> X)(x : X) -> Noo X Q x
> noo X Q x = {- Noo X Q x -}
>    elim<-> Q (\ X Q -> (x : X) -> Noo X Q x)
>      (\ x -> {- Noo WOne Refl x -}
>         noo= (moo' x {!{- Moo x -}!}))
>    x
> 
> moo : (w : WOne) -> Moo w
> moo w = {- Moo w -}
>    caseWOne w Moo \ f -> {- Moo (wrap f) -}
>      moo= (noo' (Zero -> WOne) myIso f (noo (Zero -> WOne) myIso f))
> 
> 
> 
>>
>> 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/
>> <ConorMcBride.agda>
> 
>