{"action":"created","issue":{"url":"https://api.github.com/repos/HoTT/HoTT/issues/657","labels_url":"https://api.github.com/repos/HoTT/HoTT/issues/657/labels{/name}","comments_url":"https://api.github.com/repos/HoTT/HoTT/issues/657/comments","events_url":"https://api.github.com/repos/HoTT/HoTT/issues/657/events","html_url":"https://github.com/HoTT/HoTT/issues/657","id":53032813,"number":657,"title":"Fixing `compose` and catching up with trunk","user":{"login":"JasonGross","id":396076,"avatar_url":"https://avatars.githubusercontent.com/u/396076?v=3","gravatar_id":"","url":"https://api.github.com/users/JasonGross","html_url":"https://github.com/JasonGross","followers_url":"https://api.github.com/users/JasonGross/followers","following_url":"https://api.github.com/users/JasonGross/following{/other_user}","gists_url":"https://api.github.com/users/JasonGross/gists{/gist_id}","starred_url":"https://api.github.com/users/JasonGross/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JasonGross/subscriptions","organizations_url":"https://api.github.com/users/JasonGross/orgs","repos_url":"https://api.github.com/users/JasonGross/repos","events_url":"https://api.github.com/users/JasonGross/events{/privacy}","received_events_url":"https://api.github.com/users/JasonGross/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":9,"created_at":"2014-12-29T10:42:09Z","updated_at":"2015-01-10T17:25:16Z","closed_at":null,"body":"As per [bug 3881](https://coq.inria.fr/bugs/show_bug.cgi?id=3881), we managed to catch Coq in a state where it used a different order of evar resolution than in 8.4.  With https://github.com/coq/coq/commit/96906c2a1ba9426271a4048bfa8b3991db51c192, Coq switched back to how it was doing things in 8.4, resulting in many cases of `isequiv_compose` being uninferrable.  If we β-expand `o` to make it\r\n```coq\r\nNotation compose := (fun g f x => g (f x)).\r\nNotation \"g 'o' f\" := (compose g f) (at level 40, left associativity) : function_scope.\r\n```\r\nI suspect this will be enough to fix it.  I am open to other suggestions, though.  As an example alternative, simply fixing the proofs will involve many diffs that look something like\r\n```diff\r\ndiff --git a/theories/Basics/Equivalences.v b/theories/Basics/Equivalences.v\r\nindex 5a15081..4fc64d8 100644\r\n--- a/theories/Basics/Equivalences.v\r\n+++ b/theories/Basics/Equivalences.v\r\n@@ -148,9 +148,14 @@ Global Instance symmetric_equiv : Symmetric Equiv | 0 := @equiv_inverse.\r\n (** If [g \\o f] and [f] are equivalences, so is [g].  This is not an Instance because it would require Coq to guess [f]. *)\r\n Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C}\r\n   `{IsEquiv A B f} `{IsEquiv A C (g o f)}\r\n-  : IsEquiv g\r\n+  : IsEquiv g.\r\n-  := isequiv_homotopic (compose (compose g f) f^-1)\r\n-       (fun b => ap g (eisretr f b)).\r\n+Proof.\r\n+  refine (isequiv_homotopic\r\n+            ((g o f) o f^-1)\r\n+            (fun b => ap g (eisretr f b))).\r\n+  refine (@isequiv_compose _ _ f^-1 _ _ (g o f) _).\r\n+  exact _.\r\n+Defined.\r\n\r\n Definition cancelR_equiv {A B C} (f : A -> B) {g : B -> C}\r\n   `{IsEquiv A B f} `{IsEquiv A C (g o f)}\r\n```"},"comment":{"url":"https://api.github.com/repos/HoTT/HoTT/issues/comments/69463643","html_url":"https://github.com/HoTT/HoTT/issues/657#issuecomment-69463643","issue_url":"https://api.github.com/repos/HoTT/HoTT/issues/657","id":69463643,"user":{"login":"mikeshulman","id":646600,"avatar_url":"https://avatars.githubusercontent.com/u/646600?v=3","gravatar_id":"","url":"https://api.github.com/users/mikeshulman","html_url":"https://github.com/mikeshulman","followers_url":"https://api.github.com/users/mikeshulman/followers","following_url":"https://api.github.com/users/mikeshulman/following{/other_user}","gists_url":"https://api.github.com/users/mikeshulman/gists{/gist_id}","starred_url":"https://api.github.com/users/mikeshulman/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mikeshulman/subscriptions","organizations_url":"https://api.github.com/users/mikeshulman/orgs","repos_url":"https://api.github.com/users/mikeshulman/repos","events_url":"https://api.github.com/users/mikeshulman/events{/privacy}","received_events_url":"https://api.github.com/users/mikeshulman/received_events","type":"User","site_admin":false},"created_at":"2015-01-10T17:25:16Z","updated_at":"2015-01-10T17:25:16Z","body":"Note: see discussion at #663 for what still needs fixing."}}