diff --git a/.cspell.json b/.cspell.json
index b8b17691..22dd793e 100644
--- a/.cspell.json
+++ b/.cspell.json
@@ -285,6 +285,7 @@
 		"subcollection",
 		"subconjugated",
 		"subcover",
+		"subfunctor",
 		"submanifold",
 		"submonoid",
 		"subobject",
@@ -340,8 +341,5 @@
 		"todo.txt",
 		"*.svg"
 	],
-	"ignoreRegExpList": [
-		"\\$[^$]*\\$",
-		"\\$\\$[^$]*\\$\\$"
-	]
+	"ignoreRegExpList": ["\\$[^$]*\\$", "\\$\\$[^$]*\\$\\$"]
 }
diff --git a/database/data/categories/Meas.yaml b/database/data/categories/Meas.yaml
index 6c237969..dba0996d 100644
--- a/database/data/categories/Meas.yaml
+++ b/database/data/categories/Meas.yaml
@@ -14,7 +14,6 @@ related:
 
 comments:
   - The thread <a href="https://math.stackexchange.com/questions/5024471/">MSE/5024471</a> asks for the finitely presentable objects of this category.
-  - Will Sawin has sketched a proof for the co-Malcev property in <a href="https://mathoverflow.net/questions/509552/is-the-category-mathbfring-mathrmop-a-malcev-category#comment1328251_509555">MO/509552</a>.
 
 satisfied_properties:
   - property: locally small
@@ -69,6 +68,46 @@ satisfied_properties:
 
       Finally, using <a href="/content/generator_construction">this result</a>, we conclude that the product of these two measurable spaces with underlying set $2$ is an extremal cogenerator of $\Meas$.
 
+  - property: co-Malcev
+    proof: >-
+      Let $i_1,i_2 : X \rightrightarrows R$ be a coreflexive corelation of measurable spaces. Thus, $i_1,i_2$ are jointly surjective measurable maps with a common retraction $r : R \twoheadrightarrow X$.
+      To show that $(i_1,i_2)$ is cosymmetric, define the map of sets $s : R \to R$ by
+      $$s(i_1(x)) := i_2(x), \quad s(i_2(x)) := i_1(x).$$
+      This is well-defined by a direct calculation or by using the fact that <a href="/category/Set">$\Set$</a> is co-Malcev. We need to show that $s$ is measurable. To this end, let $B \subseteq R$ be a measurable subset. Its preimages
+      $$A_1 := i_1^*(B), \quad A_2 := i_2^*(B)$$
+      are measurable subsets of $X$. We claim that
+      $$s^*(B) = \bigl((r^*(A_1) \cup r^*(A_2)) \setminus B\bigr) \cup r^*(A_1 \cap A_2), \tag{1}$$
+      which will prove in particular that $s^*(B)$ is measurable, as required. Let $y \in R$. Since $R = i_1(X) \cup i_2(X)$, we may assume without loss of generality that $y = i_1(x)$ for some $x \in X$. The following are equivalent:
+      $$y \in (r^*(A_1) \cup r^*(A_2)) \setminus B \iff x \in (A_1 \cup A_2) \setminus A_1,$$
+      $$y \in r^*(A_1 \cap A_2) \iff x \in A_1 \cap A_2.$$
+      Hence, $y$ lies in the RHS of $(1)$ if and only if
+      $$x \in ((A_1 \cup A_2) \setminus A_1) \cup (A_1 \cap A_2) = A_2 = i_2^*(B),$$
+      which means that $s(y) = i_2(x)$ lies in $B$. This proves $(1)$.
+
+      It remains to show that $(i_1,i_2)$ is cotransitive. We adopt the functorial point of view (simply to avoid talking about pushouts) and show that the subfunctor $\Hom(R,-) \hookrightarrow \Hom(X,-)^2$ is transitive. That is, given three measurable maps $u,v,w : X \rightrightrightarrows T$ into some measurable space $T$ and two measurable maps $f,g : R \rightrightarrows T$ such that
+      $$f i_1 = u, \quad f i_2 = v = g i_1, \quad g i_2 = w,$$
+      we need to show that there is a measurable map $h : R \to T$ with $h i_1 = u$ and $h i_2 = w$. We can certainly define $h$ as a map of sets by
+      $$h(i_1(x)) := u(x), \quad h(i_2(x)) := w(x),$$
+      which is well-defined by a direct calculation or again by using the fact that $\Set$ is co-Malcev. We need to show that $h$ is measurable. Let $C \subseteq T$ be a measurable subset. Its preimages
+      $$B_1 := f^*(C), \quad B_2 := g^*(C)$$
+      are measurable subsets of $R$. Notice that $f i_2 = g i_1$ implies
+      $$A := i_2^*(B_1) = i_1^*(B_2) \subseteq X.$$
+      We claim that
+      $$h^*(C) = \bigl((B_1 \cup B_2) \setminus r^*(A)\bigr) \cup (B_1 \cap B_2), \tag{2}$$
+      which will prove that $h^*(C)$ is measurable. Let $y \in R$. There are two cases to consider.
+
+      Case 1: We have $y = i_1(x)$ for some $x \in X$. The following are equivalent:
+      $$y \in (B_1 \cup B_2) \setminus r^*(A) \iff (u(x) \in C \vee v(x) \in C) \wedge v(x) \notin C,$$
+      $$y \in B_1 \cap B_2 \iff (u(x) \in C \wedge v(x) \in C).$$
+      Hence, $y$ lies in the RHS of $(2)$ if and only if $h(y) = u(x) \in C$, i.e. $y \in h^*(C)$.
+
+      Case 2: We have $y = i_2(x)$ for some $x \in X$. The following are equivalent:
+      $$y \in (B_1 \cup B_2) \setminus r^*(A) \iff (v(x) \in C \vee w(x) \in C) \wedge v(x) \notin C,$$
+      $$y \in B_1 \cap B_2 \iff (v(x) \in C \wedge w(x) \in C).$$
+      Hence, $y$ lies in the RHS of $(2)$ if and only if $h(y) = w(x) \in C$, i.e. $y \in h^*(C)$.
+
+      This proves $(2)$. We conclude that the corelation $(i_1,i_2)$ is both cosymmetric and cotransitive.
+
 unsatisfied_properties:
   - property: skeletal
     proof: This is trivial.
diff --git a/database/data/macros.yaml b/database/data/macros.yaml
index bd497850..4e71fb29 100644
--- a/database/data/macros.yaml
+++ b/database/data/macros.yaml
@@ -67,6 +67,7 @@
 \Open: \operatorname{Open}
 \Id: \operatorname{Id}
 \Br: \operatorname{Br}
+\rightrightrightarrows: \mathrel{\substack{\rightarrow\\[-0.6ex]\rightarrow\\[-0.6ex]\rightarrow}}
 
 # categories
 \Set: \mathbf{Set}