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.
Merge pull request #62 from mdnahas/master

TypeClasses for Refl, Sym, Trans applied to Paths and Equiv.
Correct arguments to equiv_compose, and simplify equiv_Transitive.
State another naming convention, and align relation instances with it
transport_forall_unwound is unnecessary