HOTT proof of transitivity of ordering of natural numbers So slowly going through HOTT book I finished chapter 1,where near the end it is defined $n \leq m \equiv \sum_{k: \mathbb{N}} a+k =_\mathbb{N} b$
Now I want to prove that if I have $a,b,c:\mathbb{N}$ such that $a \leq b$ and $b \leq c$ then $a\leq b$
Informally what I did is,I unwinded the type definition for $a \leq b$ and used transport,aka equals substituted for equals since I have that $a+k = b$ and $b+l = c$ then I substitute $b$ for $a+k$ and voila its magically done.
My problem lies in formalization of the proof by using the indiscernability of identicals.
It goes like this for every type family $$C : A  \to \mathbb{U}$$
there is a function $$f : \Pi_{x,y:A}\Pi_{p: x=_A y} C(x) \to C(y)$$
such that : $$f(x,x,refl_x) \equiv id_{C(x)} $$
Now what I basically do since by hypothesis we have given following data:
$$a,b,c : \mathbb{N}$$
$$(k,p):\sum_{k:\mathbb{N}}a+k=_\mathbb{N}b$$
$$(l,q):\sum_{l:\mathbb{N}}a+l=_\mathbb{N}b$$
Now I can define a type family $$C:\mathbb{N}\times \mathbb{N} \times \mathbb{N} \to \mathbb{U}$$ such that $$C(x,y,z) \equiv (x+y =_\mathbb{N} z )$$
Now by indiscernability of identicals there is a function $$f: \Pi_{x,y:\mathbb{N} \times \mathbb{N} \times \mathbb{N}} \Pi_{x=_{\mathbb{N} \times \mathbb{N} \times \mathbb{N}}y}C(x) \to C(y) $$
To apply this function I require a proof that triples of (a+k,l,c) and (b,l,c) are equal.But that is easy since proof of $a+k =_\mathbb{N} b$ is given by hypothesis,and second and third component are given by $refl$ proof then I can apply the function:
$$f((a+k,l,c),(a+k,l,c),refl_{(a+k,l,c)}) \equiv id_{C((a+k,l,c))}$$
Now the problems I am facing are the following.What I can do with the identity function obtained in the last line ,and is my definition of type familly sufficient,or do I need additional arguments?
How can I finish this prof?
 A: Let p1 : a+k=b, p2 :  b+l=c be the proofs given, then
f ((b,l,c),(a+k,l,c),(ap (\ x -> (x , l , c)) (sym p1))),p2) : (a+k)+l = c

So that application gets you almost all the way there, you only need the associativy of addition to obtain a+(k+l) = c.
By the way, you could use a simpler type family C(x) = x + l = c, given that you always use l and c as the last elements of the tuple.
A: I would write things as follows:
Let $i,j,k:\mathbb N$. We claim that $i\le j$ and $j\le k$ imply $i\le k$. It suffices to define 
$$
f:\left(\sum_{\ell:\mathbb N}\ (i+\ell=j)\right)\to\left(\sum_{m:\mathbb N}\ (j+m=k)\right)\to\left(\sum_{n:\mathbb N}\ (i+n=k)\right).
$$ 
It is enough to define $f((\ell,p),(m,q)):\sum_{n:\mathbb N}\ (i+n=k)$ for 
$$
\ell,m:\mathbb N,\quad p:i+\ell=j,\quad q:j+m=k.
$$ 
We set $f((\ell,p),(m,q)):\equiv(\ell+m,r)$ where $r$ is the composite of the following paths:
$\bullet$ the associativity path $i+(\ell+m)=(i+\ell)+m$, 
$\bullet$ the path $g(p):(i+\ell)+m=j+m$, where $g:\mathbb N\to \mathbb N$ is defined by $g(x):\equiv x+m$, 
$\bullet$ the path $q:j+m=k$.
