How to understand equivalence of indexes of a family of types that are not definitionally equal

Question

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?

Answer 1

We can prove (x : Nat) (y : Nat) -> 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

1. 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

2. 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.