<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <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 class="moz-txt-link-freetext" href="https://github.com/agda/agda/blob/v2.6.1/doc/user-manual/language/cubical.rst">https://github.com/agda/agda/blob/v2.6.1/doc/user-manual/language/cubical.rst</a></p>
    <p>I reached the link from
      <a class="moz-txt-link-freetext" href="https://agda.readthedocs.io/en/v2.6.1/language/cubical.html">https://agda.readthedocs.io/en/v2.6.1/language/cubical.html</a> <br>
    </p>
    <div class="moz-cite-prefix">On 05.09.20 14:06, Dan Krejsa wrote:<br>
    </div>
    <blockquote type="cite"
cite="mid:CAP7cd4CJJPcpg3CTzrfx70mJAr+c5so2EwqSPSF_Bfis3c6vkA@mail.gmail.com">
      <meta http-equiv="content-type" content="text/html; charset=UTF-8">
      <div dir="ltr">
        <div>Hi,</div>
        <div><br>
        </div>
        <div>Why isn't transp declared like this:</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> I <span class="gmail-kt"><span class="gmail-ow">→ </span>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 class="gmail-ow">→ </span></span><span class="gmail-ow"></span>A i0<span class="gmail-o"> r</span> <span class="gmail-ow">→</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"
            moz-do-not-send="true">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"
                moz-do-not-send="true">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"
                moz-do-not-send="true">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" moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
              > <a
                href="https://lists.chalmers.se/mailman/listinfo/agda"
                rel="noreferrer" target="_blank" moz-do-not-send="true">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"
            moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
          <a href="https://lists.chalmers.se/mailman/listinfo/agda"
            rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
        </blockquote>
      </div>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <pre class="moz-quote-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>
  </body>
</html>