Homotopy type theory : how to disprove that $0=\operatorname{succ}(0)$ in the type $\mathbb{N}$ $\newcommand{\suc}{\operatorname{succ}}\newcommand{\IsPrime}{\operatorname{IsPrime}}$I'm self learning Homotopy type theory reading the HoTT book. I understand that if $A+B$ and $\neg A :\equiv A\rightarrow 0$ are inhabited, then there is an inhabitant of $B$.
Proof : Compose $A\rightarrow 0$ with $0\rightarrow B$ to obtain an inhabitant of $A\rightarrow B$; one can then use the identity of $B$ to obtain an inhabitant of $B\rightarrow B$.
From $A\rightarrow B$ and $B\rightarrow B$, we obtain the type $A+B \rightarrow B$ which combined with $A+B$ gives $B$.
As an exercise, I try to prove that there is an infinite number of prime numbers.
The type I try to find an inhabitant of is
$$\prod_{n:\mathbb{N}}\sum_{p:\mathbb{N}}\IsPrime(p)\times(p>n)$$
I managed to find an inhabitant of
$$\prod_{n:\mathbb{N}}\prod_{p:\mathbb{N}} (p\leq n) + (p > n)$$
and one of
$$\prod_{n:\mathbb{N}}\sum_{p:\mathbb{N}}\IsPrime(p) \times (p\mid n! + 1)$$
From these two last types, I think I should be able to prove that $p>n$.
My strategy to do this is to deduce the type $0$ from
$$\IsPrime(p) \times (p\mid n!+1) \times (p \leq n)$$
and deduce that $p>n$ from it using the lemma at the beginning of my post.
My problem is that I only managed to find an inhabitant of $0=\suc(0)$ (here $0:\mathbb{N}$) but I cannot go further and find in inhabitant of the type $0$ from it. Is there a way to construct an inhabitant of
$$(0=\suc(0)) \rightarrow 0$$
I see no rule about the type $\mathbb{N}$ which could help me. Is it implicit in the definition of $\mathbb{N}$ or do we have to add a rule to deduce it ? In fact, as a consequence of $0=\suc(0)$, I find that every terms are equal but cannot deduce an inhabitant of $0$ from it. I think I am missing something obvious. Can someone help me ?
Thanks a lot.
 A: $\def\opn{\operatorname}$
$\def\mb{\mathbb}$
To prove this result, we shall define the observational equality principle for $\mb{N}$.

The observational equality $\opn{Eq}_{\mb{N}} : \mb{N} \rightarrow \mb{N} \rightarrow \mathcal{U}$ satisfies the following equations :
\begin{align}
\opn{Eq}_{\mb{N}}(0_\mb{N},0_\mb{N}) &:\equiv \mathbf{1} & \opn{Eq}_{\mb{N}}(\opn{succ}_{\mb{N}}(n), 0_{\mb{N}}) &:\equiv \emptyset \\
\opn{Eq}_{\mb{N}}(0_{\mb{N}}, \opn{succ}_{\mb{N}}(n)) &:\equiv \emptyset & \opn{Eq}_{\mb{N}}(\opn{succ}_{\mb{N}}(n),\opn{succ}_{\mb{N}}(m)) &:\equiv \opn{Eq}_{\mb{N}}(n, m)
\end{align}
Please note that it is also an inductive type :
\begin{align}
\opn{Eq}_{\mb{N}}(0_{\mb{N}}, m) &:\equiv \opn{E}_0(m) \\
\opn{Eq}_{\mb{N}}(\opn{succ}_{\mb{N}}(n), m) &:\equiv \opn{E}_S(n, \opn{Eq}_{\mb{N}}(n), m) 
\end{align}
with $\opn{E}_0 : \mb{N} \rightarrow \mathcal{U}$ being defined as
\begin{align}
\opn{E}_0(0_{\mb{N}}) &:\equiv \mathbf{1} \\
\opn{E}_0(\opn{succ}_{\mb{N}}(n)) &:\equiv \emptyset
\end{align}
and $\opn{E}_s$ defined as
\begin{align}
\opn{Eq}_S(n, X, 0_{\mb{N}}) &:\equiv \emptyset \\
\opn{Eq}_S(n, X, \opn{succ}_{\mb{N}}(m)) &:\equiv X(m)
\end{align}

This observational equality of the natural numbers is important because it can be used to prove equalities and inequalities.
The reflexive property of this relation, enables us to do so
$$\opn{refl-Eq}_{\mb{N}} : \prod_{n:\mb{N}} \opn{Eq}_{\mb{N}}(n, n)$$
which is again defined by induction on $\mb{N}$
\begin{align}
\opn{refl-Eq}_{\mb{N}}(0) &:\equiv \star \\
\opn{refl-Eq}_{\mb{N}}(\opn{succ}_{\mb{N}}(n)) &:\equiv \opn{refl-Eq}_{\mb{N}}(n)
\end{align}
Giving this definition, we can easily prove by induction that for $m, n : \mb{N}$
$$(m = n) \iff \opn{Eq}_{\mb{N}}(m, n)$$
Hence, it follows there is a type family $$(0_{\mb{N}} = n) \rightarrow \opn{Eq}_{\mb{N}}(0_{\mb{N}}, n)$$ indexed by $n : \mb{N}$. Thus, since $\opn{Eq}_{\mb{N}}(0_{\mb{N}}, \opn{succ}_{\mb{N}}(n)) :\equiv \emptyset$ we have $$(0_\mb{N} = \opn{succ}_{\mb{N}}(n)) \rightarrow \emptyset$$
