Internalizing Representation Independence With Univalence