Is this related to `types.Sigma.equiv_functor_sigma`?  (I haven't looked too carefully at the types to figure out if this one matches one of them exactly.)