Add Kristina's better proof that IsEquiv is an hprop.
Merge branch 'upstream' into eqvar
Merge branch 'truncequiv' into eqvar

Conflicts:
	theories/EquivalenceVarieties.v
Merge pull request #90 from mikeshulman/eqvar

Add Kristina's better proof that IsEquiv is an hprop.