How to understand equivalence of indexes of a family of types that are not definitionally equal
We can prove (x : Nat) (y : Nat) -&gt; x + y = y + x (they are propositionally equal). I'm using Agda-ish notation here rather than the notation in the HoTT book because type setting is hard. Note that we can prove this in standard intensional type theory. This gives a function from Nat to Nat to a proof of equality.

In intensional type theory we don't distinguish between types up to judgmental equality. Almost as though there's a rule

     A ≡ B  a : A
     ------------
        a : B


Remember that FZ : Fin 1, Since 0 + 1 ≡ 1, this means that FZ : Fin (0 + 1). If we didn't have a rule like this, it'd be kinda pointless to have computation in our types because the minute we actually have some interesting expression in our type we couldn't witness it.

It's important to keep the different types of equality separate in type theory


Judgmental equality (a judgement) is something actually embedded in the system. You can't touch it when writing programs but it says that two terms are equal if they have the same value more or less
Proposition equality (a proposition) is what we can prove as a programmer. There is one way to prove A = B in standard ITT, with refl : A = A. This means that we can prove A = B if and only if A and B are judgmentally equal.


Whether Fin (x + y) or Fin (y + x) for some x and y have members is dependent on what x and y. If x and y are 0, then Fin (x + y) is judgmentally equal to Fin 0, which is unoccupied.

We can prove that Fin (x + y) = Fin (y + x) though in standard ITT, the proof in a system like Agda looks like

eq : (x y : ℕ) → Fin (x + y) ≡ Fin (y + x)
eq x y rewrite +-comm x y = refl


So in answer to your question, the two types are propositionally equal using an intensional notion of equality. This isn't enough to say if e : Fin (x + y) then e : Fin (y + x), for that we'd need judgmental equality. We can easily construct invertible maps between the two though by pattern matching on the result of eq for example.

Finally, in answer to your last question. In extensional type theory this is the case, in intensional type theory we need some extra tools. HoTT in particular provides us with univalence which is even more flexible: two types can be propositionally equivalent if they're isomorphic.