<div dir="ltr"><div>Hi,</div><div><br></div><div>> Why isn't transp declared like this:</div><div>> <span>transp</span> <span>:</span> <span>∀</span> <span>{</span>ℓ<span>}</span> <span>(</span>A <span>:</span> I <span>→</span> I <span><span>→ </span>Set</span> ℓ<span>)</span> <span>(</span>r <span>:</span> I<span>)</span> <span><span>→ </span></span><span></span>A i0<span> r</span> <span>→</span> A i1 r</div><div><br></div><div>If one switches the order of the arguments of A, one gets instead</div><div><br></div><div>transp: <span>∀</span> <span>{</span>ℓ<span>}</span> <span>(</span>A <span>:</span> I <span>→</span> I <span><span>→ </span>Set</span> ℓ<span>)</span> <span>(</span>r <span>:</span> I<span>)</span> <span><span>→ </span></span><span></span>A <span>r i0</span> <span>→</span> A r i1</div><div><br></div><div>with the 'intended usage' that 'A i1 s' is definitionally independent of s.<br></div><div><br></div><div>Ignoring that condition, that looks just like a specialization of 'transport' to</div><div>the path (\i -> A r i).  Which I'm guessing means that it is not strong enough,</div><div>assuming transp is supposed to be stronger than transport.</div><div><br></div><div>From my point of view, the weird thing about the actual 'tansp' type</div><div><br></div><div><pre><span class="gmail-nf">transp</span> <span class="gmail-ow">:</span> <span class="gmail-ow">∀</span> <span class="gmail-o">{</span>ℓ<span class="gmail-o">}</span> <span class="gmail-o">(</span>A <span class="gmail-ow">:</span> I <span class="gmail-ow">→</span> <span class="gmail-kt">Set</span> ℓ<span class="gmail-o">)</span> <span class="gmail-o">(</span>r <span class="gmail-ow">:</span> I<span class="gmail-o">)</span> <span class="gmail-o">(</span>a <span class="gmail-ow">:</span> A i0<span class="gmail-o">)</span> <span class="gmail-ow">→</span> A i1<br><br></pre><pre><span style="font-family:arial,sans-serif">is one is left wondering, if A is held fix and r varies, how is<br><br>'transp A r  : A i0<span class="gmail-o"></span> <span class="gmail-ow">→</span> A i1' supposed to vary with r?<br><br></span></pre><pre><span style="font-family:arial,sans-serif">It seems in the intended usage is never that 'A is held fixed and r varies', so why<br>not encode that dependence by making the dependence of A on r explicit?<br></span></pre><pre><span style="font-family:arial,sans-serif">- Dan<br></span></pre></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Sep 7, 2020 at 3:37 AM Manuel Bärenz <<a href="mailto:manuel@enigmage.de">manuel@enigmage.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
  
    
  
  <div>
    <p>Thanks for all your comments. I've tried to compile it into a PR:
      <a href="https://github.com/agda/agda/pull/4914/" target="_blank">https://github.com/agda/agda/pull/4914/</a><br>
    </p>
    <div>On 07.09.20 12:20, Manuel Bärenz wrote:<br>
    </div>
    <blockquote type="cite">
      
      <p>Yes, that seems a good question to me as well.</p>
      <p>Relatedly: I wanted to start improving the docs, but the Github
        link is broken:
        <a href="https://github.com/agda/agda/blob/v2.6.1/doc/user-manual/language/cubical.rst" target="_blank">https://github.com/agda/agda/blob/v2.6.1/doc/user-manual/language/cubical.rst</a></p>
      <p>I reached the link from <a href="https://agda.readthedocs.io/en/v2.6.1/language/cubical.html" target="_blank">https://agda.readthedocs.io/en/v2.6.1/language/cubical.html</a>
        <br>
      </p>
      <div>On 05.09.20 14:06, Dan Krejsa wrote:<br>
      </div>
      <blockquote type="cite">
        
        <div dir="ltr">
          <div>Hi,</div>
          <div><br>
          </div>
          <div>Why isn't transp declared like this:</div>
          <div><br>
          </div>
          <div>
            <pre><span>transp</span> <span>:</span> <span>∀</span> <span>{</span>ℓ<span>}</span> <span>(</span>A <span>:</span> I <span>→</span> I <span><span>→ </span>Set</span> ℓ<span>)</span> <span>(</span>r <span>:</span> I<span>)</span> <span><span>→ </span></span><span></span>A i0<span> r</span> <span>→</span> A i1 r

</pre>
            <pre>with an intended usage that  'A s i1'  is definitionally independent of s ?
</pre>
          </div>
        </div>
        <br>
        <div class="gmail_quote">
          <div dir="ltr" class="gmail_attr">On Fri, Sep 4, 2020 at 6:17
            AM John Leo <<a href="mailto:leo@halfaya.org" target="_blank">leo@halfaya.org</a>> wrote:<br>
          </div>
          <blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
            <div dir="ltr">Thanks so much Anders for the detailed
              explanation! It's extremely helpful.
              <div><br>
              </div>
              <div>John</div>
            </div>
            <br>
            <div class="gmail_quote">
              <div dir="ltr" class="gmail_attr">On Thu, Sep 3, 2020 at
                11:09 PM Anders Mortberg <<a href="mailto:andersmortberg@gmail.com" target="_blank">andersmortberg@gmail.com</a>>
                wrote:<br>
              </div>
              <blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Yes, John's
                understanding of that very opaque error message is<br>
                correct. When checking c Agda will have to verify that
                whenever i1=i1<br>
                (that is "everywhere") then (λ i → e i) is a constant
                function. This<br>
                is clearly not the case as:<br>
                <br>
                (λ i → e i) /= (λ i → Bool)<br>
                <br>
                This is what the error message is trying to say, but e
                has been<br>
                unfolded too far and there is some mysterious
                metavariable _28.<br>
                <br>
                <br>
                Your understanding of what happens when r is i0 is also
                correct, in<br>
                that case the condition r=i1 is just i0=i1 which is
                absurd and there<br>
                is nothing to check as anything follows from an absurd
                assumption.<br>
                This is why a typechecks.<br>
                <br>
                <br>
                In general r is some element of dM(X), i.e. an element
                of the free De<br>
                Morgan algebra on some subset X of the dimension
                variables currently<br>
                in context. One way to check if some judgment holds when
                r=i1 is to<br>
                first convert r to disjunctive normal form and propagate
                the _=i1 all<br>
                the way down to the atoms. This gives us a big
                disjunction of<br>
                conjuncts where each conjunct corresponds to a list of
                substitutions.<br>
                For example if r is (i /\ j) \/ ~ k then r=i1 will
                reduce to<br>
                <br>
                ((i = i1) /\ (j = i1)) \/ (k = i0)<br>
                <br>
                To check that some judgment J holds in this context
                restriction<br>
                amounts to checking that it holds either when (i = i1)
                and (j = i1) or<br>
                when (k = i0). If I write G for the ambient context we
                hence need to<br>
                check<br>
                <br>
                G, (i = i1) /\ (j = i1) |- J<br>
                G, (k = i0) |- J<br>
                <br>
                which boils down to checking<br>
                <br>
                G |- J(i1/i)(i1/j)<br>
                G |- J(i0/k)<br>
                <br>
                I don't think Cubical Agda actually performs these
                substitutions as<br>
                it's too expensive to always substitute, but this
                intuitive algorithm<br>
                can maybe be helpful to understand how one can typecheck
                cubical<br>
                programs.<br>
                <br>
                --<br>
                Anders<br>
                <br>
                On Fri, Sep 4, 2020 at 1:05 AM John Leo <<a href="mailto:leo@halfaya.org" target="_blank">leo@halfaya.org</a>> wrote:<br>
                ><br>
                > I do have one further point I'd like clarified. Is
                the check for the r=i1 condition for transp done only
                when r is not known to be i0 or is it always done? For
                example is the check run at all when transport p
                (defined as "transp (λ i → p i) i0") is called? I assume
                not. For example in the following code<br>
                ><br>
                > notnot : (b : Bool) → not (not b) ≡ b<br>
                > notnot true  = refl<br>
                > notnot false = refl<br>
                ><br>
                > e : Bool ≡ Bool<br>
                > e = isoToPath (iso not not notnot notnot)<br>
                ><br>
                > a = transp (λ i → e i) i0 true<br>
                > b = transp (λ _ → Bool) i1 true<br>
                > c = transp (λ i → e i) i1 true<br>
                ><br>
                > I get that "a" and "b" typecheck ("a" evaluates to
                false and "b" to true as expected) but "c" fails to
                typecheck with the following error, which I assume is
                due to "e" not being definitionally constant. But
                perhaps I'm still confused.<br>
                ><br>
                > primGlue Bool<br>
                > (λ .x →<br>
                >    (λ { (i = i0) → Bool , isoToEquiv (iso not not
                notnot notnot)<br>
                >       ; (i = i1) → Bool , idEquiv Bool<br>
                >       })<br>
                >    _ .fst)<br>
                > (λ .x →<br>
                >    (λ { (i = i0) → Bool , isoToEquiv (iso not not
                notnot notnot)<br>
                >       ; (i = i1) → Bool , idEquiv Bool<br>
                >       })<br>
                >    _ .snd)<br>
                > != Bool of type Type<br>
                > when checking that the expression transp (λ i → e
                i) i1 true has<br>
                > type _28<br>
                ><br>
                ><br>
                ><br>
                > _______________________________________________<br>
                > Agda mailing list<br>
                > <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
                > <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
              </blockquote>
            </div>
            _______________________________________________<br>
            Agda mailing list<br>
            <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
            <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
          </blockquote>
        </div>
        <br>
        <fieldset></fieldset>
        <pre>_______________________________________________
Agda mailing list
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
      </blockquote>
      <br>
      <fieldset></fieldset>
      <pre>_______________________________________________
Agda mailing list
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
  </div>

_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>