Jakob von Raumer
|
28d1c6c5e4
|
chore(library/hott) move function extensionality into new axioms folder, adjust file(s) using it
|
2014-11-06 19:22:57 -05:00 |
|
Jakob von Raumer
|
02abc5c2ad
|
chore(library/hott) fixed the copyright in equiv_precomp.lean
|
2014-11-05 15:14:14 -08:00 |
|
Jakob von Raumer
|
588ad210a2
|
feat(library/hott) add theorem: assuming function extensionality, precomposing and postcomposing of equivalences is an equivalence
|
2014-11-04 18:47:34 -08:00 |
|
Jakob von Raumer
|
efa33c5b52
|
chore(library/hott) move theorem about precomposition to its own file
|
2014-11-04 18:47:34 -08:00 |
|