xy to tikz: triangular commuting diagram of two monos

subgroups.tex

@@ -85,8 +85,18 @@ \subsection{Subgroups as monomorphisms}
 \begin{lemma}
   \label{lem:setofsubgroups}
   Let $G$ be a group and $(H,i_H,!),(H',i_{H'},!):\typemono_G$ be two monomorphisms into $G$.  The identity type $(H,i_H,!)\eqto{}(H',i_{H'},!)$ is equivalent to
-  \marginnote{$$\xymatrix{H\ar[rr]^f_\simeq\ar[dr]_{i_H}&&H'\ar[dl]^{i_{H'}}\\
-    &G&}$$}
+  \marginnote{
+    \[
+      \begin{tikzpicture}[scale=1.5]
+        \path (-1,0) node (H)  {$H$}
+              (1,0)  node (H') {$H'$}
+              (0,-1) node (G)  {$G$};
+        \draw[->] (H) -- node[above] {$f$} node[below] {$\simeq$} (H');
+        \draw[->] (H) -- node[below left] {$i_H$} (G);
+        \draw[->] (H') -- node[below right] {$i_{H'}$} (G);
+      \end{tikzpicture}
+    \]
+  }
   $$\sum_{f:\Hom(H,H')}\isEq(\US f)\times (i_{H'}\eqto{}i_H f)$$ and is a proposition.
   In particular, the type $\typemono_G$ of monomorphisms into $G$ is a set.
 \end{lemma}