{"push_id":1143616871,"size":105,"distinct_size":105,"ref":"refs/heads/master","head":"0b58890b5271d68cfebb1469fe1e782f0c9033d4","before":"da6a1a786812ee0ac8c5aa49b1d25fd122029d87","commits":[{"sha":"7e64405f5e9d2a8780887432e37129c61544ca29","author":{"name":"Soonho Kong","email":"f16dc1488e12b08d983e11298e70410acf20cfee@cs.cmu.edu"},"message":"fix(emacs/lean-project.el): check project-type argument\n\nclose #1017","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/7e64405f5e9d2a8780887432e37129c61544ca29"},{"sha":"c50ab524a594ed707080fef00792641bd872318d","author":{"name":"Soonho Kong","email":"f16dc1488e12b08d983e11298e70410acf20cfee@cs.cmu.edu"},"message":"fix(emacs/lean-project.el): update prompt message, have standard as a defualt\n\nclose #1017","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/c50ab524a594ed707080fef00792641bd872318d"},{"sha":"ea775092bb600d2ec87025c3accaa9704de6236a","author":{"name":"Floris van Doorn","email":"e46576187bf87c18a08e8ae45d07379cf4db7c0f@andrew.cmu.edu"},"message":"fix(tests): use have instead of assert","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/ea775092bb600d2ec87025c3accaa9704de6236a"},{"sha":"671ef077b9497cca6d90ddc9113cbefae743d4af","author":{"name":"Floris van Doorn","email":"e46576187bf87c18a08e8ae45d07379cf4db7c0f@andrew.cmu.edu"},"message":"feat(hott): additions, mostly to types.trunc","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/671ef077b9497cca6d90ddc9113cbefae743d4af"},{"sha":"2d9c3985c9f04802da64dde972aec8ff321c9ead","author":{"name":"Floris van Doorn","email":"e46576187bf87c18a08e8ae45d07379cf4db7c0f@andrew.cmu.edu"},"message":"feat(square): add variants of eq_pathover","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/2d9c3985c9f04802da64dde972aec8ff321c9ead"},{"sha":"1e10810a1efa2ea92985c82a0e93f936b2f68d3b","author":{"name":"Floris van Doorn","email":"e46576187bf87c18a08e8ae45d07379cf4db7c0f@andrew.cmu.edu"},"message":"feat(init/funext): add function extensionality as an axiom.\n\nThis allows us to keep track of theorems which use function extensionality, but not full univalence","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/1e10810a1efa2ea92985c82a0e93f936b2f68d3b"},{"sha":"003c11c917ddbf0a13ba11651175fa36889834bc","author":{"name":"Floris van Doorn","email":"e46576187bf87c18a08e8ae45d07379cf4db7c0f@andrew.cmu.edu"},"message":"feat(connectedness): is_conn_map -> is_conn_fun, and unbundle the P in elimination principles","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/003c11c917ddbf0a13ba11651175fa36889834bc"},{"sha":"d4f0ce0eab1d29d93ac11a1d59d4d9978eaa2cd6","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"fix(library/local_context): typo","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/d4f0ce0eab1d29d93ac11a1d59d4d9978eaa2cd6"},{"sha":"5e14b4ebe838137480157dbf6ac5cfb7213e3697","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"fix(library,hott): avoid rewrite with patterns of the form (?M ...)","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/5e14b4ebe838137480157dbf6ac5cfb7213e3697"},{"sha":"0c4a6d3c5e11f59dc89cb6fd5f34b5c722b49f15","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"chore(data/set): cleanup proofs to make them less dependent on unifier heuristics","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/0c4a6d3c5e11f59dc89cb6fd5f34b5c722b49f15"},{"sha":"8f0a0d2b32b4d6ca543f21c4481989b166afbbb1","author":{"name":"Daniel Selsam","email":"8f1d6bb0bd9093ce0d9331b3ca37599085cf96af@gmail.com"},"message":"feat(library/export, doc/export_format): remove support for mutually inductive types","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/8f0a0d2b32b4d6ca543f21c4481989b166afbbb1"},{"sha":"a8db8bc61a0b00379b3d0be8ecaf0d0858dc82ee","author":{"name":"Jeremy Avigad","email":"e13e7bac66ba6b2b7fc9cbd3c8db7d6eedc7d99d@cmu.edu"},"message":"feat(library/theories/topology/filterlim): add general theory of limits, based on filters","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/a8db8bc61a0b00379b3d0be8ecaf0d0858dc82ee"},{"sha":"bd9e47c82c2938c363d304b4394211bc218a994f","author":{"name":"Ulrik Buchholtz","email":"1296d33006d4725c222242677ead3cdb335d34f1@gmail.com"},"message":"feat(hott): functoriality of pushout; connectedness in is_conn namespace\n\nother changes:\n- move result about connectedness of susp to homotopy.susp\n- improved definition of circle multiplication\n- improved the interface to join","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/bd9e47c82c2938c363d304b4394211bc218a994f"},{"sha":"bb64913e50ce44447bd92e7169517cd0893bb4ea","author":{"name":"Ulrik Buchholtz","email":"1296d33006d4725c222242677ead3cdb335d34f1@gmail.com"},"message":"feat(hott): flattening lemma for susp","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/bb64913e50ce44447bd92e7169517cd0893bb4ea"},{"sha":"0b9084c7d29454484071161245cdd3f5309d8d01","author":{"name":"Ulrik Buchholtz","email":"1296d33006d4725c222242677ead3cdb335d34f1@gmail.com"},"message":"feat(hott): hopf construction and delooping of K(G,1)s","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/0b9084c7d29454484071161245cdd3f5309d8d01"},{"sha":"d53320cb0fb4b9cda6fc3b4b490928879f94b0e6","author":{"name":"Ulrik Buchholtz","email":"1296d33006d4725c222242677ead3cdb335d34f1@gmail.com"},"message":"feat(hott): the imaginaroid version of the cayley dickson construction","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/d53320cb0fb4b9cda6fc3b4b490928879f94b0e6"},{"sha":"89296ec52a985e8c90c2df08d4d1ba49a57a643b","author":{"name":"Ulrik Buchholtz","email":"1296d33006d4725c222242677ead3cdb335d34f1@gmail.com"},"message":"feat(hott): the complex hopf fibration S3 to S2","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/89296ec52a985e8c90c2df08d4d1ba49a57a643b"},{"sha":"f11169b8f2d4430fa05b2aa42ad2d0f781e93511","author":{"name":"Ulrik Buchholtz","email":"1296d33006d4725c222242677ead3cdb335d34f1@gmail.com"},"message":"feat(hott): the quaternionic hopf fibration","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/f11169b8f2d4430fa05b2aa42ad2d0f781e93511"},{"sha":"7e8ba1440f7d8e477d22f00c96efb2a9677523a0","author":{"name":"Ulrik Buchholtz","email":"1296d33006d4725c222242677ead3cdb335d34f1@gmail.com"},"message":"feat(hott): update book.md and homotopy.md to reflect additions","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/7e8ba1440f7d8e477d22f00c96efb2a9677523a0"},{"sha":"5257e282aa2afac64f68a4f63cdd70356342f3bf","author":{"name":"Ulrik Buchholtz","email":"1296d33006d4725c222242677ead3cdb335d34f1@gmail.com"},"message":"feat(hott/homotopy): additions to sphere and susp, improve quaternionc_hopf","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-windows/commits/5257e282aa2afac64f68a4f63cdd70356342f3bf"}]}
{"actor":{"display_login":"soonhokong"}}