Floris van Doorn fec45abda5 feat(library/hott): multiple changes in the HoTT library ... Jakob accidentally undid some of my changes in commit aad4592, reverted that; made style changes in multiple files; in types/sigma: finished porting Coq-HoTT, and finished unfinished proof; in axioms/funext: rename path_forall, make arguments implicit and make instance visible		2014-12-09 21:32:35 -05:00
..
category	feat(library/hott): complete proof that object types of proper hott categories are one truncated	2014-12-05 22:21:31 -08:00
precategory	feat(library/hott): multiple changes in the HoTT library	2014-12-09 21:32:35 -05:00
binary.lean	feat(library/hott) port Jeremy's group file to use path equality	2014-12-09 10:00:37 -08:00
group.lean	feat(library/hott) port Jeremy's group file to use path equality	2014-12-09 10:00:37 -08:00
groupoid.lean	feat(library/lean) add one types as instances of groupoids	2014-12-09 19:12:54 -05:00
relation.lean	feat(library/hott) port Jeremy's group file to use path equality	2014-12-09 10:00:37 -08:00