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

[Conor McBride]

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>