{"push_id":658784912,"size":15,"distinct_size":15,"ref":"refs/heads/master","head":"a4658e60995ff7c841c7f70157d24cd85d418878","before":"1fd23e8c82adde66f6499ba9f09ae85c19107770","commits":[{"sha":"044c8bc65e00e5ef9d61e0d55d652fad654aa64f","author":{"email":"cba0fef17285386956737483f829171a211b13d9@gmail.com","name":"Mike Shulman"},"message":"the 3x3 lemma","distinct":true,"url":"https://api.github.com/repos/JasonGross/HoTT/commits/044c8bc65e00e5ef9d61e0d55d652fad654aa64f"},{"sha":"c3b1a825d6030b596cdf3353d944ad38d1198605","author":{"email":"cba0fef17285386956737483f829171a211b13d9@gmail.com","name":"Mike Shulman"},"message":"Lex modalities preserve fibers","distinct":true,"url":"https://api.github.com/repos/JasonGross/HoTT/commits/c3b1a825d6030b596cdf3353d944ad38d1198605"},{"sha":"d2b5ce39f1cf755367d6d64e1ee5b4f2e1f61faf","author":{"email":"cba0fef17285386956737483f829171a211b13d9@gmail.com","name":"Mike Shulman"},"message":"If a reflective subuniverse preserves fibers, it is a modality (and lex)","distinct":true,"url":"https://api.github.com/repos/JasonGross/HoTT/commits/d2b5ce39f1cf755367d6d64e1ee5b4f2e1f61faf"},{"sha":"bf5a8f65dfb4fd77379a6aee52889296e0df6e2c","author":{"email":"29bbaec13092d36559e3abc6f27f7d09c395819f@mit.edu","name":"Jason Gross"},"message":"Add a local admit tactic to contrib/Frudenthal.v\n\nIn 8.5beta2, the built-in [admit] which uses [proof_admitted] is\nreplaced by one aliased to [shelve]; we bring it back so we can use it\nin transparent proofs, in contrib/Freudenthal.v.","distinct":true,"url":"https://api.github.com/repos/JasonGross/HoTT/commits/bf5a8f65dfb4fd77379a6aee52889296e0df6e2c"},{"sha":"2b182865c629d4222262ec7be021d59488ee8834","author":{"email":"29bbaec13092d36559e3abc6f27f7d09c395819f@mit.edu","name":"Jason Gross"},"message":"Move [proof_admitted] out of the standard library\n\nPreparation for 8.5 beta 2.","distinct":true,"url":"https://api.github.com/repos/JasonGross/HoTT/commits/2b182865c629d4222262ec7be021d59488ee8834"},{"sha":"370896d3a323750d5c36adbf7abbe03bf723c736","author":{"email":"4ac7a4cebd6bafd29bb3ad8a20548b6705e08ab8@gmail.com","name":"Jason Gross"},"message":"Merge pull request #750 from JasonGross/fix-contrib-beta2\n\nAdd a local admit tactic to contrib/Frudenthal.v","distinct":true,"url":"https://api.github.com/repos/JasonGross/HoTT/commits/370896d3a323750d5c36adbf7abbe03bf723c736"},{"sha":"b54375c34c40d8621168f29cbbb4a4c9130f5fac","author":{"email":"cba0fef17285386956737483f829171a211b13d9@gmail.com","name":"Mike Shulman"},"message":"Add a coherence for associativity of path_prod_pp\n(Mainly to check that what I wrote in the book is correct)","distinct":true,"url":"https://api.github.com/repos/JasonGross/HoTT/commits/b54375c34c40d8621168f29cbbb4a4c9130f5fac"},{"sha":"a3c2a22967712e6f6c69564228611012d43d11f3","author":{"email":"4ac7a4cebd6bafd29bb3ad8a20548b6705e08ab8@gmail.com","name":"Jason Gross"},"message":"Merge pull request #746 from mikeshulman/lex-fibers\n\nIf a reflective subuniverse preserves fibers, it is a modality (and lex)","distinct":true,"url":"https://api.github.com/repos/JasonGross/HoTT/commits/a3c2a22967712e6f6c69564228611012d43d11f3"},{"sha":"643026b1d2f0690a3644747c5b6aa88ac10a4e3f","author":{"email":"cba0fef17285386956737483f829171a211b13d9@gmail.com","name":"Mike Shulman"},"message":"Allow repleteness of modalities to move between universes","distinct":true,"url":"https://api.github.com/repos/JasonGross/HoTT/commits/643026b1d2f0690a3644747c5b6aa88ac10a4e3f"},{"sha":"9e72d887c6d4c3217fe613c72e92c839b4f4a2ba","author":{"email":"cba0fef17285386956737483f829171a211b13d9@gmail.com","name":"Mike Shulman"},"message":"Make Lex_Reflective_Subuniverses actually instantiate SigmaClosed.\nNeeds lots of attention to universes.","distinct":true,"url":"https://api.github.com/repos/JasonGross/HoTT/commits/9e72d887c6d4c3217fe613c72e92c839b4f4a2ba"},{"sha":"13eb6b538aeee0396fa1eb5d06f5fbdd1a149d9f","author":{"email":"cba0fef17285386956737483f829171a211b13d9@gmail.com","name":"Mike Shulman"},"message":"A naive coreflective subuniverse is uniquely determined by an hprop","distinct":true,"url":"https://api.github.com/repos/JasonGross/HoTT/commits/13eb6b538aeee0396fa1eb5d06f5fbdd1a149d9f"},{"sha":"81285dbdf938c5b5afd6ea87cc61977ba9e30370","author":{"email":"9cab395a682ed00a78c031084cd2500c6701b47a@andrej.com","name":"Andrej Bauer"},"message":"Merge pull request #751 from mikeshulman/path_prod_pp_p\n\nAdd a coherence for associativity of path_prod_pp","distinct":true,"url":"https://api.github.com/repos/JasonGross/HoTT/commits/81285dbdf938c5b5afd6ea87cc61977ba9e30370"},{"sha":"1e94368f9f5421c5938882061790c5a4ff3d35fa","author":{"email":"cba0fef17285386956737483f829171a211b13d9@gmail.com","name":"Mike Shulman"},"message":"transpose a comma and a space","distinct":true,"url":"https://api.github.com/repos/JasonGross/HoTT/commits/1e94368f9f5421c5938882061790c5a4ff3d35fa"},{"sha":"8881851e34df401321b93ca60ca0f39e9f79d3c6","author":{"email":"4ac7a4cebd6bafd29bb3ad8a20548b6705e08ab8@gmail.com","name":"Jason Gross"},"message":"Merge pull request #752 from mikeshulman/lexrsu\n\nMake Lex_Reflective_Subuniverses actually instantiate SigmaClosed","distinct":true,"url":"https://api.github.com/repos/JasonGross/HoTT/commits/8881851e34df401321b93ca60ca0f39e9f79d3c6"},{"sha":"a4658e60995ff7c841c7f70157d24cd85d418878","author":{"email":"7bac9e6673174efdffb444a7f874b7f0b97e9db6@gmail.com","name":"Bas Spitters"},"message":"Merge pull request #753 from mikeshulman/coreflective\n\nA naive coreflective subuniverse is uniquely determined by an hprop","distinct":true,"url":"https://api.github.com/repos/JasonGross/HoTT/commits/a4658e60995ff7c841c7f70157d24cd85d418878"}]}