Category theory and types..? I am reading "A Gentle Introduction to Category Theory - The calculational approach"  , Marten M. Fokkinga.
In the book often a word mentioned is of "typing" and if an expressio nis well typed or not.
For eg:

A relation on Morphisms and pairs of Objects, called typing of Morphisms.


A morphism term $f$  is well typed if: a typing $f:A \to B$ can be derived for  some objects $A,B$ according to these axioms.

In other book I have never seen these concepts discussed. For eg: Paolo Perrone's Notes or Vakil's Rising Sea. How does this typing idea relate to the normal stuff?
 A: I have found the notes you are talking about. The idea of a typing is just that you like to express what kind of thing something is. For example if in a math text someone introduces a new variable n in a proof, then they will also tell you what sort of object n represents. For example they say let n be a natural number or let n be an integer. In the first case the typing of $n$ is for example $n:\mathbb N$. People which are more into set theory will probably want to write $n\in \mathbb N$, but there is a big difference between the two. A type of something is always the answer to the question "What is it?". For example someone might write down the symbol $f$, you might ask "What is $f$?" and they will tell you "Well, $f$ is a morphism from $A$ to $B$ in that category $\mathbb C$ we were talking about." Hence, the type of $f$ in that case is "morphism from $A$ to $B$" and type theorists like to denote this by $f:A\to B$. This explains the terminology in  your pdf. It really has not much content, except maybe if you want to formalize category theory in a proof assistant and need to decide if you want to use dependent types for the morphisms or whatever.The only information that the typing tells you is what codomain and domain of a morphism are.
There are some subtleties. Ignore the next paragraph if it confuses you. The thinking of many mathematicians is influenced by material set theories such as ZFC. The formal system of ZFC is single–sorted. There is only type: everything is a set. Instead of $n:\mathbb N$ set theory people would like to write $n\in \mathbb N$, but there is an important difference between the two. The expression $n\in \mathbb N$ is a statement that you can prove are refute. It is something that can be wro g or false. In contrast the information that $n$ is a set is not something you can prove or disprove. (undrr the ssumption that you are working in ZFC at this moment). It something the person has to tell you when they write down the symbol, otherwise they are just talking nonesense. Typing statements $n:\mathbb N$ are not soemthing you can disprove or prove two. They are just extra information that has to be provided when you write down the symbol. If you like to learn more about this difference, then the best setting to observe it is the difference between many–sorted and single–sorted formal first order logic.
