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

[Dan Krejsa]

Hi,

Why isn't transp declared like this:

transp : ∀ {ℓ} (A : I → I → Set ℓ) (r : I) → A i0 r → A i1 r

with an intended usage that  'A s i1'  is definitionally independent of s ?


On Fri, Sep 4, 2020 at 6:17 AM John Leo <leo at halfaya.org> wrote:

> Thanks so much Anders for the detailed explanation! It's extremely helpful.
>
> John
>
> On Thu, Sep 3, 2020 at 11:09 PM Anders Mortberg <andersmortberg at gmail.com>
> wrote:
>
>> 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
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200905/4d1be5c7/attachment.html>