leanprover/lean — pull request #316 by javra (2014-11-13 00:44:31+00:00)
Title: Ported Pointed.v, Funext_Varieties.v and a good part of UnivalenceImpliesFunext.v

UnivalenceImpliesFunext.v still lacks a proof of postcomposition with an equivlance being an equivalence that does not rely on function extensionality. This proof is weird and I will take a look at it tomorrow...