Physics, Topology, Logic and Computation: A Rosetta Stone (2009) [pdf]

Leonard Susskind's series of courses at Stanford's School of Continuing Education are a treasure. They cover the math required, but the focus is on the pure math necessary so you can move on to the next thing, and not a lot on rote calculation.

Some areas are more amenable to classical analogies than others which in turn somewhat dictates how far you can get without math. But I would say generally quantum physics just requires math if you want to get more than a very rough and superficial picture. The classical world we developed our intuitions in is just a very strange world as compared to the way nature really works at a fundamental level and so we are not well equipped to understand the world at those scales.

https://en.wikipedia.org/wiki/Mathematical_Foundations_of_Qu...

Edit: No, wait! Did you _not_ want the mathematics? On a first reading, I thought you wanted the mathematical core, without getting bogged down in practicalities around it.

2) Quantum Mechanics by A. Zagoskin

(in that order)

Both are excellent introductions into the subject, at slightly different levels (hence the order).

To me personally, type theory feels a little like an ugly definition of this initial "category with X", and I'm currently exploring in my thesis whether a syntax derived from the categorical definitions itself could also be used for the same purpose as type theory is today.

Significantly these are not just single-variable functions, or even functions whose values are real numbers; all that is necessary to describe a category is for functions to have specified domains and codomains and that any two functions with matching source and target can be composed into a third function by feeding the target of one into the source of the other, subject to the condition that composition is associative (it doesn't matter in what order you pipe the functions together), and for any object there is an identity function with from the object to itself, meaning a function which does nothing when composed with another function.

It turned out that the above axiomatization of how functions behave (i.e. that they have sources and targets and can be composed in an associative fashion) is very flexible. For example, you can essentially implement the category of linear maps (between finite-dimensional spaces) as the category whose "functions" are matrices, with source and target given by the numbers of rows or columns, and whose composition is given by matrix multiplication. Note in particular that matrices are just tables of numbers, i.e. they are not actually functions, and that the sources and targets are not the spaces themselves, but just their dimensions.

The relationship with type theory comes about as follows. The fundamental object of type theory is the type judgement "if a term x is known to be type X, and a term t is known to be of type T, then a term p(x,t) is known to be of type P". But the term p(x,t) can be understood as a function transforming a pair of terms of types T and X to a term of type P. The type judgment is then the validation that the expression p(x,t) determines a legitimate function (in the context of the specific type theory). Hence in this way, each type theory can be understood as being a syntactic presentation of a specific category of functions.