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

[Anders Mortberg]

I don't really see why this operation would be simpler to understand
than the standard transp, but what is crucial for making things work
is that we can use transp to define all of the coe^r->s operations
from cartesian cubical type theory:

https://github.com/agda/cubical/blob/master/Cubical/Foundations/CartesianKanOps.agda

--
Anders

On Mon, Sep 7, 2020 at 5:57 PM Dan Krejsa <dan.krejsa at gmail.com> wrote:
>
> 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 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 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