leanprover/lean — pull request #364 by fpvandoorn (2014-12-04 01:00:35+00:00)
Title: add characterization for pi and W types

I started porting `forall.v` in Coq HoTT to `pi.lean` and proved some basic properties of W-types (this is not from Coq HoTT (I can't find anything about W-types there), but this was for an exercise to formalize that W-types preserve `n`-truncatedness).

---

I think I start liking your suggestion about adding `abbreviation`. In `trunc.lean` I want to write
```
notation `is_hset` := is_trunc 0
```
but that requires the coercions `num -> nat -> trunc_index` which might not be loaded when `is_hset` is used, so that might give type errors.
With abbreviations, I would be able to write the following:
```
abbreviation is_hset := is_trunc 0
```
and this would typecheck in any future library, right?