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

[Manuel Bärenz]

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 i0r → 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
>> <mailto: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 <mailto: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
>>         <mailto: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 <mailto:Agda at lists.chalmers.se>
>>         > https://lists.chalmers.se/mailman/listinfo/agda
>>
>>     _______________________________________________
>>     Agda mailing list
>>     Agda at lists.chalmers.se <mailto: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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200907/cdbb5577/attachment.html>