<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">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>