{"action":"created","issue":{"url":"https://api.github.com/repos/agda/cubical/issues/180","repository_url":"https://api.github.com/repos/agda/cubical","labels_url":"https://api.github.com/repos/agda/cubical/issues/180/labels{/name}","comments_url":"https://api.github.com/repos/agda/cubical/issues/180/comments","events_url":"https://api.github.com/repos/agda/cubical/issues/180/events","html_url":"https://github.com/agda/cubical/issues/180","id":481073337,"node_id":"MDU6SXNzdWU0ODEwNzMzMzc=","number":180,"title":"How does encoding the circle loops to ints work?","user":{"login":"mrakgr","id":6266635,"node_id":"MDQ6VXNlcjYyNjY2MzU=","avatar_url":"https://avatars0.githubusercontent.com/u/6266635?v=4","gravatar_id":"","url":"https://api.github.com/users/mrakgr","html_url":"https://github.com/mrakgr","followers_url":"https://api.github.com/users/mrakgr/followers","following_url":"https://api.github.com/users/mrakgr/following{/other_user}","gists_url":"https://api.github.com/users/mrakgr/gists{/gist_id}","starred_url":"https://api.github.com/users/mrakgr/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mrakgr/subscriptions","organizations_url":"https://api.github.com/users/mrakgr/orgs","repos_url":"https://api.github.com/users/mrakgr/repos","events_url":"https://api.github.com/users/mrakgr/events{/privacy}","received_events_url":"https://api.github.com/users/mrakgr/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":22,"created_at":"2019-08-15T09:38:00Z","updated_at":"2019-08-15T14:23:22Z","closed_at":null,"author_association":"NONE","body":"```\r\n{-# OPTIONS --cubical --safe #-}\r\nopen import Cubical.Core.Everything\r\n\r\nopen import Cubical.Foundations.Prelude\r\n\r\nopen import Cubical.Data.Nat\r\nopen import Cubical.Data.Int\r\n\r\ndata S¹ : Type₀ where\r\n  base : S¹\r\n  loop : base ≡ base\r\n\r\nhelix : S¹ → Type₀\r\nhelix base     = Int\r\nhelix (loop i) = sucPathInt i\r\n\r\nencode : base ≡ base → Int\r\nencode p = transport (λ i → helix (p i)) (pos zero)\r\n\r\nq : encode loop ≡ encode (sym loop ∙ loop ∙ loop)\r\nq = refl\r\n```\r\n\r\nI can't wrap my head around this. I can see that if you compose `n` `sucPathInt`s, you would get path that increments `n` times rather than just once when doing the transport. But path constructors themselves can't have such computational context. They are more like AST nodes rather than actual operations.\r\n\r\nWith AST nodes you could interpret them in order to get the same behavior as for regular operations, but I can't see how this is happening.\r\n\r\n```\r\nhelix (loop i) = sucPathInt i\r\n```\r\n\r\nThere is the `sucPathInt` and that answers the question of where it is happening, but I can't see how this connects to everything else.\r\n\r\nIt is not like transport is iterating over a list and counting the number of `loop` occurrences. In `encode p = transport (λ i → helix (p i)) (pos zero)` won't `p i` always be `base`?"},"comment":{"url":"https://api.github.com/repos/agda/cubical/issues/comments/521659483","html_url":"https://github.com/agda/cubical/issues/180#issuecomment-521659483","issue_url":"https://api.github.com/repos/agda/cubical/issues/180","id":521659483,"node_id":"MDEyOklzc3VlQ29tbWVudDUyMTY1OTQ4Mw==","user":{"login":"mrakgr","id":6266635,"node_id":"MDQ6VXNlcjYyNjY2MzU=","avatar_url":"https://avatars0.githubusercontent.com/u/6266635?v=4","gravatar_id":"","url":"https://api.github.com/users/mrakgr","html_url":"https://github.com/mrakgr","followers_url":"https://api.github.com/users/mrakgr/followers","following_url":"https://api.github.com/users/mrakgr/following{/other_user}","gists_url":"https://api.github.com/users/mrakgr/gists{/gist_id}","starred_url":"https://api.github.com/users/mrakgr/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mrakgr/subscriptions","organizations_url":"https://api.github.com/users/mrakgr/orgs","repos_url":"https://api.github.com/users/mrakgr/repos","events_url":"https://api.github.com/users/mrakgr/events{/privacy}","received_events_url":"https://api.github.com/users/mrakgr/received_events","type":"User","site_admin":false},"created_at":"2019-08-15T14:23:22Z","updated_at":"2019-08-15T14:23:22Z","author_association":"NONE","body":"Before I turn my attention to `helix` again, there is something I am wondering about.\r\n\r\n```\r\n{-# OPTIONS --cubical #-}\r\n\r\nopen import Cubical.Core.Everything\r\nopen import Cubical.Foundations.Prelude\r\n\r\nopen import Cubical.Data.Nat\r\n\r\ndata ℤ : Set where\r\n  pos : (n : ℕ) → ℤ\r\n  neg : (n : ℕ) → ℤ\r\n  posneg : pos 0 ≡ neg 0\r\n\r\nsucℤ : ℤ → ℤ\r\nsucℤ (pos n) = pos (suc n)\r\nsucℤ (neg zero) = pos 1\r\nsucℤ (neg (suc n)) = neg n\r\nsucℤ (posneg i) = pos 1\r\n```\r\n\r\nAt first I thought this was completely straightforward, but now I see that I misunderstood it. Originally what I thought was that what this was saying is that since `ℤ` has `posneg : pos 0 ≡ neg 0` as a path constructor that would act as an assertion at compile time that `sucℤ (pos 0)` and `sucℤ (neg 0)`.\r\n\r\nBut if that was really the case, for what reason is the `sucℤ (posneg i) = pos 1` case even necessary? It should be possible to infer whether that is true from the rest of the cases. Also I never really understood where that `i` is coming from in path constructors.\r\n\r\n```\r\nsucℤ : ℤ → ℤ\r\nsucℤ (pos zero) = pos 2\r\nsucℤ (pos (suc n)) = pos (suc (suc n))\r\nsucℤ (neg zero) = pos 3\r\nsucℤ (neg (suc n)) = neg n\r\nsucℤ (posneg i) = {!!}\r\n```\r\n```\r\nGoal: ℤ\r\n————————————————————————————————————————————————————————————\r\ni : I\r\n———— Constraints ———————————————————————————————————————————\r\n(pos 2) = (?0 (i = i0)) : ℤ\r\n(pos 3) = (?0 (i = i1)) : ℤ\r\n```\r\n\r\nOnly now do I see that it is trying to link the two sides.\r\n\r\nWhat is unusual here is that this is what one would get if one was trying to prove an equality. It does not at all resemble destructuring a inductive type. Rather this is where a path type is being created.\r\n\r\nActually there seems to be more at work here...\r\n\r\n```\r\nsuc 2       suc 3\r\n  |          |\r\n  |          |\r\n  |          |\r\nsuc 2 ----- suc 3\r\n```\r\n\r\nAssuming you could get this to typecheck, that would not only be proof that the horizontal equalities hold, but also that the vertical ones do as well. Obviously the above cannot be true.\r\n\r\n```\r\nsuc 1       suc 1\r\n  |          |\r\n  |          |\r\n  |          |\r\nsuc 1 ----- suc 1\r\n```\r\n\r\nIn the original program it is trivial. In the `helix`, it is less so.\r\n\r\n```\r\nhelix : S¹ → Type₀\r\nhelix base     = Int\r\nhelix (loop i) = sucPathInt i\r\n```\r\n\r\nIn this function the equality box would look something like...\r\n\r\n```\r\nInt                 Int\r\n |                   |\r\n |                   |\r\n |                   |\r\nsucPathInt i0 ----- sucPathInt i1\r\n```\r\n\r\nA few posts ago I wrote that I was confused about something...\r\n\r\n```\r\nhelix (p i)\r\nhelix (loop i)\r\nhelix base\r\nInt\r\n```\r\n\r\n```\r\nhelix (p i)\r\nhelix (loop i)\r\nsucPathInt i\r\n```\r\n\r\nNamely, that the first one is what I would expect the thing to reduce, but the second one is the thing that seems to be executing. Based on the behavior it seems like the truth should be...\r\n\r\n```\r\nhelix (p i)\r\nhelix (loop i)\r\nhelix base\r\nInt\r\nsucPathInt i\r\n```\r\n\r\nBecause `helix base` needs to equal its path constructor case (for both `i0` and `i1`) hence `Int` can be transported to `sucPathInt i`."}}
{"actor":{"display_login":"mrakgr"}}