adding [Funext-comp-rules.v], a discussion of computation rules for functional extensionality.
Folding content of [Funext-comp-rules.v] into [Funext.v].
Removing [Funext-comp-rules.v].
Personalising readme.
Added statement of [contr_funext], and proof of it from [funext_dep].
Merge branch 'master' of github.com:peterlefanulumsdaine/HoTT
Trying to understand Ltac second-order pattern-matching
Joining the dots from naive to strong funext.
Fixing breakage in prev commit
Major reorganisation of Funext.v
Adding archive copy of blog post menagerie.html
Adding derivation(s) of dependent from non-dependent W-types.
Renaming to w-to-inductive.v to make use of builtin equality explicit.
Starting on fetooling of w-to-inductive.v without rewrite; ack, it’s painful.
Minor correction to previous commit.
Committing changes that were over a very old version of upstream, for later re-basing.
Added theorem [forall_hlevel], that h-levels are closed under arbitrary products.
Minor proof simplifications (lemmas about hprops are instances of lemmas about general h-levels).
Merge pull request #29 from peterlefanulumsdaine/pll_master

Added lemma [forall_hlevel], that h-levels are closed under arbitrary products.
Make the code work with the latest coq + univ polymorphism. Stopping
in Univalence due to a universe inconistency/unification issue, not
sure which yet.