leanprover/lean — pull request #288 by fpvandoorn (2014-11-04 00:47:45+00:00)
Title: major changes in library

I made some major changes in the library. I wanted to wait with pushing until I had finished the formalization of the slice functor, but for some reason that is very hard to formalize, requiring a lot of casts and manipulation of casts. So I've not finished that yet.

Changes:
- in multiple files make more use of `variables`
- move dependent `congr_arg` theorems to `logic.cast` and proof them using `heq` (which doesn't involve nested inductions and fewer casts).
- prove some more theorems involving `heq`, e.g. `hcongr_arg3` (which do not require `piext`)
- in theorems where casts are used in the statement use `eq.rec_on` instead of `eq.drec_on`
- in `category` split `basic` into `basic`, `functor` and `natural_transformation`
- change the definition of `functor` to use fully bundled categories. @avigad: this means that the file `semisimplicial.lean` will also need changes (but I'm quite sure nothing major). You want to define the fully bundled category Delta, and use only fully bundled categories (`type` and `ᵒᵖ` are notations for the fully bundled `Type_category` and `Opposite` if you open namespace `category.ops`). If you want I can make the changes.
- lots of minor changes

(sorry for the unhelpful commit message, I was not sure what to write there)