The degree to which one would see this as a major downside would be strongly correlated with the factors that cause one to start taking HRT. There is a popular TERF narrative that detransitioners universally realise that everything was a mistake and regret the physical changes. From observation, however, this is rare and, if there's any concrete concrete identifiable reason for detransition like "I found Jesus Christ", detransitioners tend to not express significant levels of distress about the fact that they experienced physical changes.
I need to read about Benabou's perspective more, but otherwise I think that indexing and dependent types is just a syntactic layer used to describe fibrations. I explain this for about 15min in this timestamp of a recent talk of mine: https://youtu.be/vLCvrXJDPys?si=wxgLc_AZGsQmh93G&t=869
The catch is that fibring (n+1)-simplices (n+2)-separate times over n-simplices is the wrong way to form the fibration. One instead wants to form the matching object of (n+1)-simplex boundaries as a limit of the previous dimension data and fibre over it once. If you watch that excerpt from the talk, then I translate how to go from the indexed type-theoretic definition to that of a fibration.