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