f_equal should be transparent to be used conveniently in homotopy proofs
misplaced 'admit' in a multigoal proof
Rewriting of the original Paths.v of the HoTT library,  with a lot of comments.
This alternative version is placed in a sub-directory of ssrplugin, since
it depends on the ssrplugin tactics and libs.
dep in Logic_Type
Added names for resp and invp
minor comment on why we can use rewrite for non dpt cases
Updating Fibrations.v, keeping the names, statements and body of lemmas as unchanged as possible (still, using the groupish notations introduced in Paths.v)
removed some forgotten 'Defined'
Modified Contractible. Shorten proof that two parallel paths in a contractible set are homotopic
modified a comment
added a comment for my not understanding why hfiber and fibration do not use the same construction wrt to eta
removed deprecated comment in Fibration + removed the dependency of Contractible on Fibration
A new version of Contractible with structures inspired from Cyril's dev
More comments
Installation instructions reflect the fact that we have a non-working Coq right now
Placing datatypes into Type
small lemma on id =1 f instead of f =1 id + typos in comments
initial import of Equivalence.v (WIP)
Nicer proofs about Equivalences by Cyril&Assia.

- using transport to define eq_equiv
- use of equiv_rect as the default elimination principle for <~>, see
  proofs of compK and compVK.
- study of the elementary properties of pre/post composition with (e \o e^-1)
  when e is an equivalence under univalence axiom.
- use the previous to simplify dramatically the proof that projections
  of the diagonal are equal (1 line) and subsequent 2-line proof of
  functional extensionality.
- complete and shorten proof of ~UIP (originally by Anders Mörtberg).
More comments and small improvements:

- explaination about why even defining a function with a seamingly
  inocuous rewrite may create trouble (see transport in Fibrations.v)

- improved (simpler) definition of concat2 in Paths.v

- more comments in Equivalence.v, in part. about canonical structure
  and the proof of funext.