Categorical interpretation of equality type Consider the Martin Lof type theory.
It's know that:
product type correspond to product of two obects;
unit type correspond to terminal object;
and so on.
The equality type corresponds to some categorical construction?
 A: The short answer is, for non-dependent type theories, equality is a left adjoint (in the bicategory of fibred categories over a fixed base) of pullback along the diagonal, $\delta : A\to A\times A$, which is contraction.  For dependent type theories and identity types, we need a "dependent" contraction which we can characterize as the mediating morphism of a weakening projection along itself.  Except the (fibred) left adjoint to this only gives you a "weak" notion, so an additional condition is applied.  The "weakness" (not to be confused with "weakening") is essentially that the type that we are eliminating into is not dependent on the value we are eliminating.  This issue happens with all left adjoints of this form.  Seeing how all this relates to type theory requires looking at the categorical semantics of type theories, in particular of types/terms in context, which is non-trivial.  Getting identity types as opposed to just equality requires the semantics of dependent type theories which is even less trivial.
Doing a whirlwind tour omitting many details and using a particularly simple case of fibration, we can think of a type in context, $\Gamma \vdash B$, as an object of the slice category $\mathcal{C}/\Gamma$.  A term in context, $\Gamma, x:B \vdash M : C$, is an arrow of $\mathcal{C}/\Gamma$ from $\Gamma \vdash B$ to $\Gamma \vdash C$ (so $x$ is not free in $C$, this is what causes the "weakness").  We also have arrows of $\mathcal{C}$,  $\sigma : \Delta\to\Gamma$ which give rise to (pseudo)functors $\sigma^* : \mathcal{C}/\Gamma\to\mathcal{C}/\Delta$ by pulling back along $\sigma$.  I.e. an object of $\mathcal{C}/\Gamma$ is an arrow $(\Gamma, x:B)\to\Gamma$ and we get an arrow $(\Delta, x: B[\sigma]) \to \Delta$ from the left arrow in the following pullback diagram, where I'm using $B[\sigma]$ to mean the term $B$ with the substitution $\sigma$ applied to it.
$$\require{AMScd}
\begin{CD}
(\Delta,x:B[\sigma]) @>>> (\Gamma,x:B) \\
@VVV @VVV \\
\Delta @>>\sigma> \Gamma
\end{CD}$$
Incidentally, $\mathcal{C}\simeq\mathcal{C}/1$ so we can think of arrows of $\mathcal{C}$ as terms in the empty context. Also, "weakening" is the pullback functor along a projection which will add a(n unused) variable to the context, $\pi^* : \mathcal{C}/\Gamma \to \mathcal{C}/(\Gamma, x:A)$. The notation $\Gamma, x:A$ and such for arrows is just a suggestive way of writing (in the non-dependent case) $\Gamma\times A$.
Now we have $\delta : A \to A\times A$, so we have the pullback functor $$(id_\Gamma\times\delta)^* : \mathcal{C}/(\Gamma, x:A,y:A)\to\mathcal{C}/(\Gamma,z:A)$$  In type theory notation,
$$\frac{\Gamma, x : A, y : A \vdash B}{\Gamma,z : A \vdash B[x\mapsto z,y\mapsto z]}$$
$(id_\Gamma\times\delta)^*$ being a right adjoint means that we have the following two rules; the first representing one direction of the isomorphism of homsets defining an adjunction, natural in $C$, and the other being the counit.  That's all that's necessary to completely specify the adjunction.  Also, to simplify the display slightly, I cheated a bit by choosing source of the arrow in $\mathcal{C}/(\Gamma,x:A)$ to be $\Gamma,x:A\vdash 1$ and then omitting it.  (This is actually cheating since a fibre-wise $1$, i.e. a unit type, may not exist, but we almost always have it, so it's not cheating by much and, as naturality would indicate, it wouldn't really have mattered what it was.)
$$\frac{\quad \Gamma,x : A, y : A \vdash C \qquad \Gamma,z:A \vdash M : C[x\mapsto z,y\mapsto z]}{\Gamma,x : A, y: A, p:x =_A y \vdash J(M[z\mapsto x];x,y,p) : C}$$
$$\frac{\Gamma \vdash A}{\Gamma, x:A \vdash \mathbf{refl}_x : x =_A x}$$ If you compare the rule for $J$ with, for example, the one on nlab, it will seem too simple.  Partially because of the $\Delta$ which I've omitted (because we're not actually in a dependently typed context quite yet, and, as is stated on that page, it is unnecessary if we have dependent products).  However, there's also the fact that $C$ and $M$ don't depend on the identity type we're eliminating!  It's easier to get an idea of the consequence of this by considering the coproduct case.  If our eliminator's return type isn't parameterized by the coproduct type (in this example) we're eliminating, then we can't do a case analysis at the type level, to have a different return type depending on the eliminated value. (b : Bool) -> if b then Int else Bool is a perfectly legitimate type in Agda.  This is what makes this formulation "weak".  I'm not going to cover what's necessary to get "strong" identity types, but any introduction to categorical semantics of type theory will.  Another thing I haven't explained is what extra conditions are necessary to get a fibred adjunction, i.e. one that behaves correctly if we modify $\Gamma$.  These conditions are the Beck-Chevalley conditions.
To upgrade this to get an actual dependent type theory, the main thing we need to do is change what we mean by "weakening", or rather the projections that underlie it.  By using the normal projection $\pi : \Gamma\times A \to \Gamma$, we are essentially saying $A$ is independent of $\Gamma$ because $\pi$ is natural in $\Gamma$.  We need something that will project $\Gamma$ out of a $(\Gamma, x:A)$ where $A$ may be intertwined with $\Gamma$.  These are called display maps. A comprehension category, in particular, says among other things that for any type-in-context, I can give you a projection which will allow you to extend the context with that type (with which you can make new types that depend on that type and its context).  Of course, one of the main enablers of dependently typed programming is dependent product types which are fibred right adjoints to weakening.
The dictionary of the relation between logic, type theory, and category theory on nLab may be of interest to you, as well as the description of the categorical semantics of dependent types.  The prospectus to Bart Jacobs' book, Categorical Logic and Type Theory, is a decent and relatively pleasant introduction to these ideas.  If you are serious about pursuing categorical semantics, I would recommend his book or his thesis, but they are rough going (particularly his thesis).  You would probably want to complement his thesis with other resources, for example, Andrew Pitts' notes on Categorical Logic.
A: To the best of my knowledge, equality can be characterized as the unique solution to the following universal characterisation: equality is the least equivalence relation; i.e.,
$$\forall \text{ equivalence relation} \sim \;\bullet \; \forall x,y \;\bullet\; x = y \implies x \sim y $$
Now the notion of `least' just means that there are certain unique arrows from the object being defined. So it remains to define the notion of equivalence internally. Some possible routes are by co-equalizers while another is by groupoids.
Best of luck!
