 
 (defn context-xia-product
   "Computes Xia's product of ctx-1 and ctx-2, where for two contexts
-  $(G_1,M_1,I_1)$ and $(G_2,M_2,I_2)$ their Xia product is defined as
-  \\[
-    (G_1\\times G_2, M_1\\times M_2, \\tilde)
-  \\]
+  (G_1,M_1,I_1) and (G_2,M_2,I_2) their Xia product is defined as
+
+    (G_1 x G_2, M_1 x M_2, ~)
+
   where
-  \\[
-    (g_1,g_2) \\tilde (m_1,m_2) \\iff (g_1I_1m_1\\iff g_2I_2m_2).
-  \\]."
+
+    (g_1,g_2) ~ (m_1,m_2) <=> (g_1I_1m_1 <=> g_2I_2m_2).
+  "
   [ctx-1 ctx-2]
   (let [G_1 (objects ctx-1)
         G_2 (objects ctx-2)


(defn context-semiproduct
  "Computes the context semiproduct of ctx-1 and ctx-2, where for
  contexts $(G_1,M_1,I_1)$ and $(G_2,M_2,I_2)$ their semidirect
  product is defined as
  \\[
    (G_1\\times G_2, M_1\\cup M_2, \\nabla)
  \\]
  where
  \\[
    (g_1,g_2)\\nabla(j,m) \\iff g_jI_jm \\qquad\\text{for $j\\in\\set{1,2}$}.
  \\]"
  [ctx-1 ctx-2]
  (let [new-objs (cross-product (objects ctx-1) (objects ctx-2))
        new-atts (disjoint-union (attributes ctx-1) (attributes ctx-2))


(defn context-composition
  "Returns context composition of ctx-1 and ctx-2, that is

    (G_1,M_1,I_1) o (G_2,M_2,I_2) := (G_1,M_2,I_1 o I_2).
  "
  [ctx-1 ctx-2]
  (make-context-nc (objects ctx-1)
                   (attributes ctx-2)
