HOTT proof of transitivity of ordering of natural numbers

Question

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?

Answer 1

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.

Answer 2

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$.