I checked the type, and this is not `equiv_functor_sigma`. Probably `equiv_sigT_rect` is the right thing here, although it's more dependent than it needs to be.