[Agda] Fwd: Fwd: Question about transport and cubical

[Anders Mortberg]

Yes, John's understanding of that very opaque error message is
correct. When checking c Agda will have to verify that whenever i1=i1
(that is "everywhere") then (λ i → e i) is a constant function. This
is clearly not the case as:

(λ i → e i) /= (λ i → Bool)

This is what the error message is trying to say, but e has been
unfolded too far and there is some mysterious metavariable _28.


Your understanding of what happens when r is i0 is also correct, in
that case the condition r=i1 is just i0=i1 which is absurd and there
is nothing to check as anything follows from an absurd assumption.
This is why a typechecks.


In general r is some element of dM(X), i.e. an element of the free De
Morgan algebra on some subset X of the dimension variables currently
in context. One way to check if some judgment holds when r=i1 is to
first convert r to disjunctive normal form and propagate the _=i1 all
the way down to the atoms. This gives us a big disjunction of
conjuncts where each conjunct corresponds to a list of substitutions.
For example if r is (i /\ j) \/ ~ k then r=i1 will reduce to

((i = i1) /\ (j = i1)) \/ (k = i0)

To check that some judgment J holds in this context restriction
amounts to checking that it holds either when (i = i1) and (j = i1) or
when (k = i0). If I write G for the ambient context we hence need to
check

G, (i = i1) /\ (j = i1) |- J
G, (k = i0) |- J

which boils down to checking

G |- J(i1/i)(i1/j)
G |- J(i0/k)

I don't think Cubical Agda actually performs these substitutions as
it's too expensive to always substitute, but this intuitive algorithm
can maybe be helpful to understand how one can typecheck cubical
programs.

--
Anders

On Fri, Sep 4, 2020 at 1:05 AM John Leo <leo at halfaya.org> wrote:
>
> 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
>
> notnot : (b : Bool) → not (not b) ≡ b
> notnot true  = refl
> notnot false = refl
>
> e : Bool ≡ Bool
> e = isoToPath (iso not not notnot notnot)
>
> a = transp (λ i → e i) i0 true
> b = transp (λ _ → Bool) i1 true
> c = transp (λ i → e i) i1 true
>
> 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.
>
> primGlue Bool
> (λ .x →
>    (λ { (i = i0) → Bool , isoToEquiv (iso not not notnot notnot)
>       ; (i = i1) → Bool , idEquiv Bool
>       })
>    _ .fst)
> (λ .x →
>    (λ { (i = i0) → Bool , isoToEquiv (iso not not notnot notnot)
>       ; (i = i1) → Bool , idEquiv Bool
>       })
>    _ .snd)
> != Bool of type Type
> when checking that the expression transp (λ i → e i) i1 true has
> type _28
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda