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



Homotopy type theory : how to disprove that $0=\operatorname{succ}(0)$ in the type $\mathbb{N}$
$\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$$


