[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

If one switches the order of the arguments of A, one gets instead

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

with the 'intended usage' that 'A i1 s' is definitionally independent of s.

Ignoring that condition, that looks just like a specialization of
'transport' to
the path (\i -> A r i).  Which I'm guessing means that it is not strong
enough,
assuming transp is supposed to be stronger than transport.

>From my point of view, the weird thing about the actual 'tansp' type

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

is one is left wondering, if A is held fix and r varies, how is

'transp A r  : A i0 → A i1' supposed to vary with r?

It seems in the intended usage is never that 'A is held fixed and r
varies', so why
not encode that dependence by making the dependence of A on r explicit?

- Dan



On Mon, Sep 7, 2020 at 3:37 AM Manuel Bärenz <manuel at enigmage.de> wrote:

> Thanks for all your comments. I've tried to compile it into a PR:
> https://github.com/agda/agda/pull/4914/
> On 07.09.20 12:20, Manuel Bärenz wrote:
>
> Yes, that seems a good question to me as well.
>
> Relatedly: I wanted to start improving the docs, but the Github link is
> broken:
> https://github.com/agda/agda/blob/v2.6.1/doc/user-manual/language/cubical.rst
>
> I reached the link from
> https://agda.readthedocs.io/en/v2.6.1/language/cubical.html
> On 05.09.20 14:06, Dan Krejsa wrote:
>
> 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
>>
>
> _______________________________________________
> Agda mailing listAgda at lists.chalmers.sehttps://lists.chalmers.se/mailman/listinfo/agda
>
>
> _______________________________________________
> Agda mailing listAgda at lists.chalmers.sehttps://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/20200907/366189e8/attachment.html>