<html>
  <head>
    <meta content="text/html; charset=ISO-8859-1"
      http-equiv="Content-Type">
  </head>
  <body bgcolor="#FFFFFF" text="#000000">
    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).<br>
    <br>
    Empty := mu X.X<br>
    <br>
    Box := mu X. (Empty -&gt; X)<br>
    <br>
    Note that X occurs positively in the body of the mu-type for Box.&nbsp;
    The theory gives us a recursor R with this typing rule<br>
    <br>
    b : Box<br>
    f : (Empty -&gt; T) -&gt; T<br>
    ---------------------<br>
    R(b,f) : T<br>
    <br>
    We certainly have the isomorphism Box = (Empty -&gt; Box) -- it is
    even a definitional equality! -- but we cannot use this recursor to
    write a term of type Box -&gt; Empty.&nbsp; The best we could do would be
    to start like this, where g has type Empty -&gt; Empty, and hence is
    useless for deriving Empty.<br>
    <br>
    loop = \ b . R(b, \ g . (g ?))<br>
    <br>
    So I think the wrap constructor being used in Maxime's code is just
    an explicit witness of the above implicit isomorphism.&nbsp; Removing it
    should not count for structural decrease (obviously).<br>
    <br>
    Cheers,<br>
    Aaron<br>
    <br>
    <div class="moz-cite-prefix">On 01/08/2014 11:53 AM, Andreas Abel
      wrote:<br>
    </div>
    <blockquote cite="mid:52CD90B4.40804@ifi.lmu.de" type="cite">
      <pre wrap="">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 &lt;-&gt; X

But you say it is justified, is it?

Cheers,
Andreas

On 07.01.2014 17:42, Conor McBride wrote:
</pre>
      <blockquote type="cite">
        <blockquote type="cite">
          <pre wrap="">Very good. Agda is right and Coq got it wrong. As I said previosuly the
definition of loop implicitely uses K.
</pre>
        </blockquote>
        <pre wrap="">
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 -&gt; WOne) -&gt; WOne

data _&lt;-&gt;_ (X : Set) : Set -&gt; Set where
   Refl : X &lt;-&gt; X

postulate
   myIso : WOne &lt;-&gt; (Zero -&gt; WOne)

moo : WOne -&gt; Zero
noo : (X : Set) -&gt; (WOne &lt;-&gt; X) -&gt; X -&gt; Zero

moo (wrap f) = noo (Zero -&gt; WOne) myIso f
noo .WOne Refl x = moo x

bad : Zero
bad = moo (wrap \ ())
</pre>
      </blockquote>
      <pre wrap="">
</pre>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <br>
      <pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
    <br>
  </body>
</html>