Théorie homotopique des types

Bonjour,
Alors voila je me presente je suis en L3 de math et depuis la fin de l'année dernière je commence a m'interesser a la logique. Je n'ai lus aucun cours mais bon a mon niveau, je me suis mis a y reflechir ( surtout sur le tiers exlus ) et j'ai un peu avancé dans ma reflexion.

Ce matin, je suis tombé sur cet article : http://images.math.cnrs.fr/A-la-croisee-des-fondements-des.html
Ce n'est pas vraiment de la logique mais voila, ca m'a donné envie d'en savoir plus sur cette fameuse Théorie Homolotique des types.
Etant donnée que ce n'est pas quelque chose qu'on apprend en cours, je me suis donnée comme objectif de la comprendre ( même si cela dois me prendre 3 ans).

Je me suis donc un peu renseigné pour savoir par ou commencer.
J'ai décidé de commencer par la theorie des types puisque j'ai en ce moment des cours de topo ( qui me menerons a la topo algebrique puis aux homotopie).
J'en ai deduit qu'il faut d'abord que je lise du Russell puis Godel pour enfin arriver a la théorie des types de Per Martin-Löf.
Alors voila j'aimerais savoir si il y a des bouquins qui regroupe tout cela pour la théorie des types ou si il faut que je lise les livres de chaques mathématiciens?
Me faut il des prerequis pour me lancer dans cette theorie?

Merci d'avance,
Jorisder