GitHub PushEvent at 2014-12-06 07:27:13
Repository: lean-osx
Actor: soonhokong
Payload: {"shas":[["5fe8ee606f715415dcc38ab6c4d36e366527e435","dbf64074c535b6b84a73384ad297d5521819740f@web.de","feat(library/hott): port Floris' category implementation","Jakob von Raumer",true],["d8e2206bbc356321e2de8b01f34759c43303d3d7","dbf64074c535b6b84a73384ad297d5521819740f@web.de","feat(library/hott): try to replace the proof irrelevance","Jakob von Raumer",true],["ae618c20fb89123f6cbb38daec68262347379827","dbf64074c535b6b84a73384ad297d5521819740f@web.de","fix(library/hott): finish associativity proof","Jakob von Raumer",true],["67f71ee37649199c20dfed5095dfce662591f4ce","dbf64074c535b6b84a73384ad297d5521819740f@web.de","feat(library/hott): finish porting of natural_transformation.lean","Jakob von Raumer",true],["a1b468d104aff668f462c1b7efa2ae8779d8fd8d","dbf64074c535b6b84a73384ad297d5521819740f@web.de","feat(library/hott): port a part of algebra/category/constructions.lean, slice category still to do","Jakob von Raumer",true],["9631c6b1a121e3f8058b255fb5289e3c21ead65a","dbf64074c535b6b84a73384ad297d5521819740f@web.de","feat(library/hott): add iso_of_path lemma for precategories","Jakob von Raumer",true],["b37a77d25e55eb79b9313d09791ee3b10e6a10c3","dbf64074c535b6b84a73384ad297d5521819740f@web.de","chore(library/hott): move precategory definition to its own folder","Jakob von Raumer",true],["cda828bfe8ce6687e53ac355bbb17db1abe4b374","dbf64074c535b6b84a73384ad297d5521819740f@web.de","chore(library/algebra): change category to be a structure","Jakob von Raumer",true],["6124b878701b0fb642c7d8777ca9096e40e8fb60","dbf64074c535b6b84a73384ad297d5521819740f@web.de","fix(library/hott): adjust expliciteness of arguments","Jakob von Raumer",true],["91862926e3252d1f77953fafe744ad1e133e72d2","dbf64074c535b6b84a73384ad297d5521819740f@web.de","chore(library/hott): change precategory to structure, fix morphism.lean","Jakob von Raumer",true],["39ba9429f5484b717af1b8265790037e24ee2610","dbf64074c535b6b84a73384ad297d5521819740f@web.de","chore(library/hott): make constructions.lean compile, still lots of work to do","Jakob von Raumer",true],["dbce41114a0ae6b2383fb317f6442cae6edf342a","dbf64074c535b6b84a73384ad297d5521819740f@web.de","feat(library/hott): add definition of category","Jakob von Raumer",true],["63afac301cd07c83d7385331467a3ee23983daaf","dbf64074c535b6b84a73384ad297d5521819740f@web.de","chore(library/hott): turn isomorphic into structure","Jakob von Raumer",true],["59233923952e4c939805031b8a28f89b7cba16a4","dbf64074c535b6b84a73384ad297d5521819740f@web.de","chore(library/hott): make precategory use the isomorphic structure","Jakob von Raumer",true],["aad4592cad766fcf0a575830ad0e687803fb39c8","dbf64074c535b6b84a73384ad297d5521819740f@web.de","feat(library/hott): complete theorems about truncatedness of isomorphism sets","Jakob von Raumer",true],["cc2de8a8d940acb47d80da9b0dda6472c5875171","dbf64074c535b6b84a73384ad297d5521819740f@web.de","feat(library/hott): complete proof that object types of proper hott categories are one truncated","Jakob von Raumer",true],["7c1b75c8182a681ec54dcd2fe61115cd8af3c282","dbf64074c535b6b84a73384ad297d5521819740f@web.de","feat(library/hott): add proof that the type of nat trafos is a set\n\nThe characteriszation of nat trafo by sigma types up to equivalence is still to be done (two unsuccessful proof attempts included)","Jakob von Raumer",true],["133f935fce0c771dec69caf0e844816dcf243abd","dbf64074c535b6b84a73384ad297d5521819740f@web.de","fix(library/hott): issues resulting from merge","Jakob von Raumer",true],["75b312954f39081feaaf87d27062b0cca3ba9351","1b60d2ed7158736cbc1353d72a6dc44a6772147f@travis-ci.org","fix(library/hott): issues resulting from merge","Travis CI",true]],"size":19,"ref":"refs/heads/master","head":"75b312954f39081feaaf87d27062b0cca3ba9351"}