{"action":"created","issue":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/194","labels_url":"https://api.github.com/repos/UniMath/UniMath/issues/194/labels{/name}","comments_url":"https://api.github.com/repos/UniMath/UniMath/issues/194/comments","events_url":"https://api.github.com/repos/UniMath/UniMath/issues/194/events","html_url":"https://github.com/UniMath/UniMath/issues/194","id":112155637,"number":194,"title":"computing with weq's","user":{"login":"DanGrayson","id":700228,"avatar_url":"https://avatars.githubusercontent.com/u/700228?v=3","gravatar_id":"","url":"https://api.github.com/users/DanGrayson","html_url":"https://github.com/DanGrayson","followers_url":"https://api.github.com/users/DanGrayson/followers","following_url":"https://api.github.com/users/DanGrayson/following{/other_user}","gists_url":"https://api.github.com/users/DanGrayson/gists{/gist_id}","starred_url":"https://api.github.com/users/DanGrayson/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/DanGrayson/subscriptions","organizations_url":"https://api.github.com/users/DanGrayson/orgs","repos_url":"https://api.github.com/users/DanGrayson/repos","events_url":"https://api.github.com/users/DanGrayson/events{/privacy}","received_events_url":"https://api.github.com/users/DanGrayson/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":4,"created_at":"2015-10-19T14:25:12Z","updated_at":"2015-10-19T23:09:28Z","closed_at":null,"body":"One may sometimes define an equivalence as a composite of a chain of weq's and inverses of weq's.  Here is an example:\r\n```\r\nDefinition total2_step {n} (X:stn (S n) -> UU) :\r\n  (Σ i, X i) ≃ (Σ (i:stn n), X (dni _ (lastelement _) i)) ⨿ X (lastelement _).\r\nProof.\r\n  intros. set (f := weqdnicoprod n (lastelement _)).\r\n  intermediate_weq (Σ x : stn n ⨿ unit, X (f x)).\r\n  { apply invweq. apply weqfp. }\r\n  intermediate_weq ((Σ i, X (f (ii1 i))) ⨿ Σ t, X (f (ii2 t))).\r\n  { apply weqtotal2overcoprod. }\r\n  apply weqcoprodf. { apply weqfibtototal; intro i. apply idweq. }\r\n  apply weqtotal2overunit.\r\nDefined.\r\n```\r\n\r\nNow suppose you want to compute something about it.  Then it becomes a problem that the various weq's used and their inverses don't always compute immediately.  Here are two lemmas showing the situation with ```weqfp```:\r\n```\r\n(* Learn how to compute with\r\n      weqfp { X Y : UU } ( w : X ≃ Y )(P:Y-> UU) : (Σ x : X, P (w x)) ≃ (Σ y, P y)  \r\n   and its inverse. *)\r\n\r\nDefinition weqfp_compute_1 { X Y : UU } ( w : X ≃ Y )(P:Y-> UU) (xp: Σ x,P(w x)) :\r\n  weqfp w P xp = (w (pr1 xp),,pr2 xp).\r\nProof. reflexivity. Defined.\r\n\r\nDefinition weqfp_compute_2 { X Y : UU } ( w : X ≃ Y )(P:Y-> UU) (yp:Σ y,P y) :\r\n  invmap (weqfp w P) yp = (invmap w (pr1 yp),,transportf P (! homotweqinvweq w (pr1 yp)) (pr2 yp)).\r\nProof. intros. induction yp as [y p].\r\n  intermediate_path (invmap (weqfp w P) (_,,transportf P (! homotweqinvweq w y) p)).\r\n  { apply maponpaths. eapply total2_paths; reflexivity. }\r\n  exact (homotinvweqweq _ (_,,_)).\r\nDefined.\r\n```\r\n\r\nI propose improving the definition of ```weqfp``` by adding a step at the end where we replace the inverse map by the simple formula for it, displayed above.  I think that would make computations easier, because then one could just unfold ```invmap``` and ```weqfp``` to reveal the result, instead of rummaging around for a computation proposition.\r\n\r\nThis procedure might help with computability of lots of weq's in the system.\r\n\r\nComments?"},"comment":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/comments/149372698","html_url":"https://github.com/UniMath/UniMath/issues/194#issuecomment-149372698","issue_url":"https://api.github.com/repos/UniMath/UniMath/issues/194","id":149372698,"user":{"login":"vladimirias","id":424011,"avatar_url":"https://avatars.githubusercontent.com/u/424011?v=3","gravatar_id":"","url":"https://api.github.com/users/vladimirias","html_url":"https://github.com/vladimirias","followers_url":"https://api.github.com/users/vladimirias/followers","following_url":"https://api.github.com/users/vladimirias/following{/other_user}","gists_url":"https://api.github.com/users/vladimirias/gists{/gist_id}","starred_url":"https://api.github.com/users/vladimirias/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/vladimirias/subscriptions","organizations_url":"https://api.github.com/users/vladimirias/orgs","repos_url":"https://api.github.com/users/vladimirias/repos","events_url":"https://api.github.com/users/vladimirias/events{/privacy}","received_events_url":"https://api.github.com/users/vladimirias/received_events","type":"User","site_admin":false},"created_at":"2015-10-19T23:09:28Z","updated_at":"2015-10-19T23:09:28Z","body":">  I propose improving the definition of weqfp by adding a step at the end\n> > where we replace the inverse map by the simple formula for it, displayed\n> > above.\n\nYou mean to apply it to your definition of an equivalence where the inverse map is part of the structure?\n\n\n\n\n\n\n> On Oct 19, 2015, at 12:03 PM, Daniel R. Grayson <notifications@github.com> wrote:\n> \n> Yes, that's always the first step of such a proof.\n> \n> On Mon, Oct 19, 2015 at 11:39 AM, Vladimir Voevodsky <\n> notifications@github.com> wrote:\n> \n> > Dan, have you use the fact that to compare two weq’s it is sufficient to\n> > compare the corresponding functions, i.e., if (f, is) and (g, is’) are weqs\n> > then f=g implies that (f,is)=(g,is1). Similarly one can prove a lemma that\n> > the same holds for the function components of invweq.\n> >\n> > Vladimir.\n> >\n> >\n> >\n> > > On Oct 19, 2015, at 10:25 AM, Daniel R. Grayson <\n> > notifications@github.com> wrote:\n> > >\n> > > One may sometimes define an equivalence as a composite of a chain of\n> > weq's and inverses of weq's. Here is an example:\n> > >\n> > > Definition total2_step {n} (X:stn (S n) -> UU) :\n> > > (Σ i, X i) ≃ (Σ (i:stn n), X (dni _ (lastelement _) i)) ⨿ X (lastelement\n> > _).\n> > > Proof.\n> > > intros. set (f := weqdnicoprod n (lastelement _)).\n> > > intermediate_weq (Σ x : stn n ⨿ unit, X (f x)).\n> > > { apply invweq. apply weqfp. }\n> > > intermediate_weq ((Σ i, X (f (ii1 i))) ⨿ Σ t, X (f (ii2 t))).\n> > > { apply weqtotal2overcoprod. }\n> > > apply weqcoprodf. { apply weqfibtototal; intro i. apply idweq. }\n> > > apply weqtotal2overunit.\n> > > Defined.\n> > > Now suppose you want to compute something about it. Then it becomes a\n> > problem that the various weq's used and their inverses don't always compute\n> > immediately. Here are two lemmas showing the situation with [weqfp]:\n> > >\n> > > (* Learn how to compute with\n> > > weqfp { X Y : UU } ( w : X ≃ Y )(P:Y-> UU) : (Σ x : X, P (w x)) ≃ (Σ y,\n> > P y)\n> > > and its inverse. *)\n> > >\n> > > Definition weqfp_compute_1 { X Y : UU } ( w : X ≃ Y )(P:Y-> UU) (xp: Σ\n> > x,P(w x)) :\n> > > weqfp w P xp = (w (pr1 xp),,pr2 xp).\n> > > Proof. reflexivity. Defined.\n> > >\n> > > Definition weqfp_compute_2 { X Y : UU } ( w : X ≃ Y )(P:Y-> UU) (yp:Σ\n> > y,P y) :\n> > > invmap (weqfp w P) yp = (invmap w (pr1 yp),,transportf P (!\n> > homotweqinvweq w (pr1 yp)) (pr2 yp)).\n> > > Proof. intros. induction yp as [y p].\n> > > intermediate_path (invmap (weqfp w P) (_,,transportf P (! homotweqinvweq\n> > w y) p)).\n> > > { apply maponpaths. eapply total2_paths; reflexivity. }\n> > > exact (homotinvweqweq _ (_,,_)).\n> > > Defined.\n> > > I propose improving the definition of weqfp by adding a step at the end\n> > where we replace the inverse map by the simple formula for it, displayed\n> > above. I think that would make computations easier, because then one could\n> > just unfold [invmap] and [weqfp] to reveal the result, instead of rummaging\n> > around for a computation proposition.\n> > >\n> > > This procedure might help with computability of lots of weq's in the\n> > system.\n> > >\n> > > Comments?\n> > >\n> > > —\n> > > Reply to this email directly or view it on GitHub <\n> > https://github.com/UniMath/UniMath/issues/194>.\n> > >\n> >\n> > —\n> > Reply to this email directly or view it on GitHub\n> > <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_UniMath_UniMath_issues_194-23issuecomment-2D149252582&d=BQMFaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=PAZ_jTPLrSb1btCfAu4RkycWe57N0sGyzbjgeOn2wN0&m=VnZw3-lYBquO7WIUxjMx_4pKfJ-5tJQ4732lfb2ur0E&s=Xg9-5YrUBD6_Oa4gfT2TaECbW6dAMXQLfjlanwAmdgw&e=>\n> > .\n> >\n> —\n> Reply to this email directly or view it on GitHub <https://github.com/UniMath/UniMath/issues/194#issuecomment-149259444>.\n> \n\n"}}