[Agda] Fwd: Fwd: Question about transport and cubical
Manuel Bärenz
manuel at enigmage.de
Mon Sep 7 12:20:48 CEST 2020
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200907/db81b0ae/attachment.html>
More information about the Agda
mailing list