I have a feeling that homotopy type theory might be a better foundation for music theory. For instance, two pitches an octave apart are often described as equal, but it's a non-trivial equality. One might say that there is a "path" between them. Different chord inversions are also "equal" in this sense. A thirteenth chord can be identified with an added sixth, and so on. Then there are chords that are missing the third or the fifth. Such chords can be idenitified using more than one path, so you may have higher homotopies.