fix: equation labels

blueprint/src/chapter/natural_model.tex

@@ -301,7 +301,7 @@ \subsection{Identity types}
 	\arrow["{\Star{\rho}_{\Type}}"', from=2-1, to=2-2]
 \end{tikzcd}
 \begin{equation}
-    \label{diag:J_definition_diagram}
+    \label{eq:JDefinition1}
 \end{equation}
 \end{center}
 Taking the pullback $T$ and the comparison map $\ep$ we have
@@ -321,7 +321,7 @@ \subsection{Identity types}
 	\arrow["{\Star{\rho}_{\Type}}"', from=3-2, to=3-3]
 \end{tikzcd}
 \begin{equation}
-  	\label{diag:J_definition}
+  	\label{eq:JDefinition2}
 \end{equation}
 \end{center}
 Finally, we require a section $\J : T \to \Poly{q}{\Term}$ of $\ep$,
@@ -834,7 +834,7 @@ \subsection{Stability of the universe under type formers}
 The left face of the outer cube is the composed diagonal pullback square from
 \ref{diag:universe-identity-type-classifier-pullback-cube}.
 The front face of the outer cube is the naturality square for $\Star{\rho}$ from
-\ref{diag:J_definition}
+\ref{eq:JDefinition2}
 and similarly the back face is the naturality square for $\Star{\rho_{U}}$ from
 \ref{diag:J_U_definition}.
 
@@ -1088,7 +1088,7 @@ \subsection{Extensional identity types and UIP}
 	\arrow["\Id"', from=2-1, to=2-2]
 \end{tikzcd}\end{center}
 Note that this means $\Star{\rho}$ is an isomorphism,
-from which it follows that \ref{diag:J_definition_diagram} is also a pullback,
+from which it follows that \ref{eq:JDefinition1} is also a pullback,
 i.e. $\ep$ is an isomorphism.
 % https://q.uiver.app/#q=WzAsNCxbMCwwLCJcXFBvbHl7cX0ge1xcVGVybX0iXSxbMCwxLCJcXFBvbHl7cX0ge1xcVHlwZX0iXSxbMSwxLCJcXFBvbHl7XFx0cH0ge1xcVGVybX0iXSxbMSwwLCJcXFBvbHl7XFx0cH0ge1xcVGVybX0iXSxbMCwxLCJcXFBvbHl7cX0ge1xcdHB9IiwyXSxbMSwyLCJcXFN0YXJ7XFxyaG99X3tcXFR5cGV9IiwyXSxbMywyLCJcXFBvbHl7XFx0cH0ge1xcdHB9Il0sWzAsMywiXFxTdGFye1xccmhvfV97XFxUZXJtfSJdLFswLDIsIiIsMSx7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dXQ==
 \begin{center}\begin{tikzcd}