There are several things one can learn when going into homotopy theory.
Since I don't know how much you already know about these kinds of topics I will include many possible things you could do.
On the one hand I think it is worthwhile to get familiar with simplicial sets (do you know them?) and their relationship with topological spaces.
A good (In my view from the modern language the best) reference is "Simplicial Homotopy Theory" by Goerss and Jardine.
When studying the relationship to topological spaces now it depends on how much homotopy theory you already know.
You should learn about CW complexes, fibrations, homotopy groups, the Hurewicz theorem, the Whitehead theorem, the long exact sequence of a fibration, the factorization via the cylinder and the homotopy fiber, CW approximations and Postnikow-sections.
I suppose all of this is treated at least in the book "Elements of homotopy theory" by G.W. Whitehead. Propably there are also newer treatments of this, for example "Modern Classical homotopy theory" by J. Strom. I don't know this book myself, but a good friend of mine has read in it.
Then what you could learn next, I think, would be the language of model categories.
A good introduction is the paper by Dwyer and Spalinski called "Homotopy theory and model categories" ( here is a link to a pdf http://folk.uio.no/paularne/SUPh05/DS.pdf )
Then in the book of Goerss and Jardine in chapters 1 and 2 you will learn a lot about this and the importance of simplicial sets in this business.
It is worthwile to learn many examples of model categories (e.g. Top with Quillen model structure, Top with Strom model structure, Chain complexes, simplicial sets, sequential spectra...)
After all of this the next thing to lean into could be foundations in stable homotopy theory. But for the moment I think this is enough already.
If you tell me what you already know, maybe I could give a more precise suggestion of what to learn next, as I figure what I've told you is about 2 or 3 courses and a seminar :)
Hope it helps a little bit,
Best regards
The usual names for $\Sigma$-types and $\Pi$-types are dependent sum and dependent product, respectively, but for some reason the Homotopy Type Theory book calls them dependent pair type and dependent function type.
Whatever you call them, they respectively generalise binary products and exponentiation: $X \times Y$ is just the sum of $X$-many copies of $Y$, i.e. $\sum_{x : X} Y$, and $Y^X$ is the product of $X$-many copies of $Y$, i.e. $\prod_{x : X} Y$.
Best Answer
You didn't exactly ask "what background do I need to learn HoTT", but since that's the question some other people are answering, I'll address that too. The subject as a whole is quite wide, and if to understand it all and its applications deeply would require significant background in homotopy theory, higher category theory, topos theory, and type theory. However, none of that is necessarily required at the beginning, and indeed learning HoTT may help you get a handle on those other subjects at the same time or later on.
The book Homotopy type theory was written with the intent of assuming as few prerequisites as possible, not even basic algebraic topology or type theory, although it does assume some mathematical maturity and perhaps more category theory than would be ideal. If you don't have any exposure to category theory, I would recommend doing a bit of reading there; some good introductory books are Awodey's Category theory and Leinster's Basic category theory. But other than that, I would suggest diving into the HoTT Book and see how you find it. The first chapter of the HoTT Book is an introduction to type theory, intended to stand on its own; it's necessarily brief and only covers the basics necessary for the rest of the book, so you may want to supplement it with other readings, but unfortunately really good introductions to type theory are hard to find.
The HoTT Book is only about one particular facet of the subject, namely developing mathematics internally to HoTT. If you want to learn about semantics, for instance, you'll have to go elsewhere, and eventually need more background in abstract homotopy theory and higher category theory. May's book is not an unreasonable place to go after Hatcher; particularly because May uses the modern language of category theory (which Hatcher seems unaccountably allergic to), which is also at the basis of HoTT. Beware that Concise lives up to its name and requires a lot of the reader. The sequel More concise algebraic topology is mostly not hugely relevant for HoTT, but it does contain a good introduction to model categories, which you'll have to learn about eventually if you want to understand the semantics of HoTT.
Finally, as I mentioned in the comments, I also suggest availing yourself of the other resources linked at the homotopytypetheory.org web site, which include several video lectures and basic introductions written for people with differing backgrounds.