So I've been reading things about HoTT and trying to get solid on the foundations before getting too much further into the book. I am confused by a certain point; maybe I just haven't read far enough yet however. I don't think my question is specific to HoTT but just dependent type theory in general.
Say you have a family of types defined by something like $B : Nat \to Set$. There are two fibers/indexed types defined by $B(x + y)$ and $B(y + x)$. These are definitely not definitionally equivalent but maybe they are extensionally equivalent because $x + y = y + x$. However I thought that perhaps indexes behave definitionally in some cases in which case $B(x + y)$ and $B(y + x)$ might be extensionally distinct.
I tried thinking about the case of $Fin : Nat \to Set$ (the integers less than a certain value). I think that both $Fin (x + y)$ and $Fin (y + x)$ have no inhabitants however because the standard constructors for them have no constructors that unify with $x + y$ or $y + x$. So they both have no inhabitants but what does that mean about their equivalence? This seemed like a bad case to think about to me.
My main question is the following: how does one think about the equivalence between these two types?
My subquestions/confusions are: Do these types have the same inhabitants? Are they extensionally equal? Does having the same inhabitants means that types are extensionally equal?