GitHub PushEvent at 2014-04-29 05:01:07
Repository: HoTT
Actor: JasonGross
Payload: {"shas":[["8a261878e402f97a5fed278bd2d9b14ce3ae515b","29bbaec13092d36559e3abc6f27f7d09c395819f@mit.edu","Fix timing files to deal with negative times","Jason Gross",false],["b740f1c1efd3aa64c0eb4942c576683aab651b5f","29bbaec13092d36559e3abc6f27f7d09c395819f@mit.edu","Add some lemmas and tactics for removing isos\n\nThis is the main tactic used to prove that lax comma categories are\nprecategories.  Unfortunately, it's sometimes rather slow.  It could\nprobably benefit from reflective automation.\n\nThis closes #383","Jason Gross",true],["c5e705728b67db90b250676a611268b9ac59bd6f","29bbaec13092d36559e3abc6f27f7d09c395819f@mit.edu","Vastly simplify the helper-tactics in Category/Morphisms.v\n\nWe don't actually need all of those; I was being stupid with\nassociativity.","Jason Gross",true],["6e6dd36ec7c132017f1218e7c31cb8ff07899f47","29bbaec13092d36559e3abc6f27f7d09c395819f@mit.edu","Add some helper lemmas about [commutes]","Jason Gross",true]],"size":4,"ref":"refs/heads/misc-lemmas","head":"6e6dd36ec7c132017f1218e7c31cb8ff07899f47"}