Add category of ω-sets

.cspell.json

@@ -34,6 +34,7 @@
 		"algebraicity",
 		"algébriques",
 		"anneaux",
+		"Aronszajn",
 		"Artin",
 		"Auslander",
 		"Axiomatising",
@@ -169,6 +170,7 @@
 		"deloopings",
 		"Demazure",
 		"Diers",
+		"diagonalization",
 		"diffeomorphism",
 		"diffeomorphisms",
 		"disjointness",
@@ -244,6 +246,7 @@
 		"irreflexive",
 		"Isbell",
 		"isos",
+		"Jaap",
 		"Johnstone",
 		"Jónsson",
 		"Kashiwara",
@@ -291,6 +294,7 @@
 		"Noetherian",
 		"Noncommutative",
 		"objectwise",
+		"Oosten",
 		"opfibration",
 		"Perrone",
 		"pointwise",

content/cocongruences_in_extensive_categories.md

@@ -0,0 +1,173 @@
+---
+title: Cocongruences in extensive categories
+description: This gives some results on cocongruences in extensive categories with various extra hypotheses.
+---
+
+# Cocongruences in extensive categories
+
+We start with a general fact which is easier to visualize for the dual case of congruences.
+
+::: Lemma 1
+Let $q_1, q_2 : E \rightrightarrows X$ be a congruence such that the pullback $E \times_X E$ of $q_2$ and $q_1$ exists, and let $t : E \times_X E \to E$ be the transitivity morphism. Then we have pushout diagrams
+
+$$
+\begin{CD}
+E \times_X E @> p_1 >> E @. \quad @. E \times_X E @> p_2 >> E \\
+@V t VV @VV q_1 V @. @V t VV @VV q_2 V \\
+E @> q_1 >> X @. \quad @. E @> q_2 >> X.
+\end{CD}
+$$
+
+:::
+
+::: Proof
+Suppose we have a commutative square
+
+$$
+\begin{CD}
+E \times_X E @> p_1 >> E \\
+@V t VV @VV f V \\
+E @> g >> T.
+\end{CD}
+$$
+
+Then for any generalized element $(x, y)$ of $E$, consider the generalized elements $((x, x), (x, y))$ and $((x, y), (y, y))$ of $E \times_X E$. From the commutativity of the square acting on these generalized elements, we have
+$$f(x, x) = g(x, y)$$
+and
+$$f(x, y) = g(x, y).$$
+Therefore, if we define $h : X \to T$ on generalized elements by $h(x) \coloneqq f(x, x)$, we must have $f = h \circ q_1$ and $g = h \circ q_1$. Conversely, if $h$ is a morphism with $f = h \circ q_1$, we have $h(x)=f(x,y)$ for all $(x,y) \in E$, which for $y=x$ yields $h(x)=f(x,x)$.
+
+This concludes the proof that the first diagram is a pushout diagram; the proof for the second is similar.
+:::
+
+::: Lemma 2
+Suppose we have two pullback diagrams
+
+$$
+\begin{CD}
+A_1 @> f_1 >> B @. \quad @. A_2 @> f_2 >> B \\
+@V g_1 VV @VV h V @. @V g_2 VV @VV h V \\
+C_1 @> k_1 >> D @. \quad @. C_2 @> k_2 >> D
+\end{CD}
+$$
+
+in an extensive category. Then we can combine these into a pullback diagram
+
+$$
+\begin{CD}
+A_1 + A_2 @> (f_1; f_2) >> B \\
+@V g_1 + g_2 VV @VV h V \\
+C_1 + C_2 @> (k_1; k_2) >> D.
+\end{CD}
+$$
+
+:::
+
+::: Proof
+Suppose we have compatible maps $T \to B$ and $T \to C_1 + C_2$. Then using extensivity, we can find a decomposition of the latter into morphisms $T_1 \to C_1$ and $T_2 \to C_2$ where $T \cong T_1 + T_2$. Using the individual pullback diagrams, we can then construct morphisms $T_1 \to A_1$ and $T_2 \to A_2$ with the corresponding projections to $B, C_1, C_2$. The sum $T \cong T_1 + T_2 \to A_1 + A_2$ then gives the required morphism for the desired pullback diagram. On the other hand, the uniqueness of this morphism $T \to A_1 + A_2$ follows from the uniqueness conditions for $T_1 \to A_1$ and $T_2 \to A_2$ from the assumed pullback diagrams, along with the disjointness of the coproduct $C_1 + C_2$ (to be exact, the fact that the coprojections $C_1 \to C_1 + C_2$ and $C_2 \to C_1 + C_2$ are monomorphisms).
+:::
+
+::: Corollary 3
+Let $j_1, j_2 : X \rightrightarrows E$ be a cocongruence in an extensive category such that the pushout $E +_X E$ of $j_2$ and $j_1$ exists, and let $t : E \to E +_X E$ be the corresponding cotransitivity morphism. Then we have a pullback diagram
+
+$$
+\begin{CD}
+X + X @> (j_1; j_2) >> E \\
+@V j_1 + j_2 VV @VV t V \\
+E + E @>>> E +_X E.
+\end{CD}
+$$
+
+In particular, if the category also has pullback-stable regular epimorphisms, then for any cocongruence $j_1, j_2 : X \rightrightarrows E$, the corresponding morphism $(j_1; j_2) : X + X \to E$ is a regular epimorphism.
+:::
+
+::: Proof
+The pullback diagram comes from using Lemma 2 on the two pullback diagrams from the dual of Lemma 1. For the other conclusion, all we need to establish is that $E + E \to E +_X E$ is a regular epimorphism. This follows from the construction of the pushout $E +_X E$ of monomorphisms (in fact, split monomorphisms with the coreflexivity morphism being the left inverse) as a quotient of a congruence on $E + E$ <a href="/content/pushouts-of-monos-via-congruence-quotients">here</a>.
+:::
+
+In the following results, define a <i>regular corelation</i> to be a corelation $j_1, j_2 : X \rightrightarrows E$ such that the binary copower of $X$ exists, and $(j_1; j_2) : X + X \to E$ is a regular epimorphism.
+
+::: Lemma 4
+In an extensive category, every regular coreflexive corelation $j_1, j_2 : X \rightrightarrows E$ such that the equalizer of $j_1$ and $j_2$ exists is an effective cocongruence.
+:::
+
+::: Proof
+Let $e : Y \hookrightarrow X$ be the equalizer of $j_1$ and $j_2$. We will prove that the parallel pair
+
+$$
+\begin{align*}
+(i_1; i_1 \circ e; i_2 \circ e; i_2) & ,\\
+(i_1; i_2 \circ e; i_1 \circ e; i_2) & : X + Y + Y + X \rightrightarrows X + X.
+\end{align*}
+$$
+
+is a kernel pair of $(j_1; j_2) : X + X \to E$.
+Informally, we can think of this as the subobject of $(X + X)^2 \cong \sum_{i,j=1}^2 X^2$ which is the diagonal of $X$ in the first and fourth quadrants, and the diagonal of $Y$ in the second and third quadrants.
+
+To see this, note that since $j_1$ is a (split) monomorphism, we have a pullback diagram
+
+$$
+\begin{CD}
+X @> \id >> X \\
+@V \id VV @VV j_1 V \\
+X @>> j_1 > E.
+\end{CD}
+$$
+
+Similarly, since $e$ is formed as a coreflexive equalizer, we have a pullback diagram
+
+$$
+\begin{CD}
+Y @> e >> X \\
+@V e VV @VV j_1 V \\
+X @>> j_2 > E.
+\end{CD}
+$$
+
+(See <a href="/category-implication/pullbacks_imply_coreflexive_equalizers">here</a>.)
+
+Combining these using Lemma 2, we get a pullback diagram
+
+$$
+\begin{CD}
+X+Y @> (\id; e) >> X \\
+@V \id + e VV @VV j_1 V \\
+X+X @>> (j_1; j_2) > E.
+\end{CD}
+$$
+
+Similarly, we get a pullback diagram
+
+$$
+\begin{CD}
+Y+X @> (e; \id) >> X \\
+@V e + \id VV @VV j_2 V \\
+X+X @>> (j_1; j_2) > E.
+\end{CD}
+$$
+
+Now, combining those two using Lemma 2 (transposed), we get a pullback diagram
+
+$$
+\begin{CD}
+(X+Y)+(Y+X) @> (\id; e) + (e; \id) >> X+X \\
+@V (\id+e; e+\id) VV @VV (j_1; j_2) V \\
+X+X @>> (j_1; j_2) > E.
+\end{CD}
+$$
+
+However, under the canonical isomorphism $(X+Y)+(Y+X) \cong X+Y+Y+X$, we see that $(\id; e) + (e; \id)$ corresponds to
+$$(i_1; i_1\circ e; i_2\circ e; i_2) : X+Y+Y+X \to X+X,$$
+whereas $(\id+e; e+\id)$ corresponds to
+$$(i_1; i_2\circ e; i_1\circ e; i_2) : X+Y+Y+X \to X+X.$$
+
+Therefore, since $(j_1; j_2) : X + X \to E$ is a regular epimorphism, it is a coequalizer of this kernel pair. However, this coequalizer is exactly the congruence quotient in the construction <a href="/content/pushouts-of-monos-via-congruence-quotients">here</a> of $X +_Y X$. Thus, we see that the original corelation is equivalent to the cokernel pair of $e$.
+:::
+
+::: Corollary 5
+In an extensive and regular category with quotients of congruences, every cocongruence is effective.
+:::
+
+::: Proof
+This follows by combining Corollary 3 and Lemma 4, using the existence of quotients of congruences so that $E +_X E$ always exists by <a href="/content/pushouts-of-monos-via-congruence-quotients">this result</a>.
+:::

database/data/categories/Bin.yaml

@@ -90,40 +90,6 @@ satisfied_properties:
       which is a contradiction.
     label: Bin_extremal_cogenerator
 
-  - property: effective cocongruences
-    proof: >-
-      Let $q_1,q_2 : (X,R) \rightrightarrows (Y,S)$ be a cocongruence. Since the forgetful functor $\Bin \to \Set$ is cocontinuous, the pair $q_1,q_2 : X \rightrightarrows Y$ is a cocongruence in <a href="/category/Set">$\Set$</a>, which has effective cocongruences and equalizers. Thus, if $E \subseteq X$ denotes the equalizer of $q_1,q_2$, the canonical map
-      $$\alpha : X \sqcup_E X \to Y,\qquad i_1(x) \mapsto q_1(x),\quad i_2(x) \mapsto q_2(x)$$
-      is bijective. This is the underlying map of the canonical morphism
-      $$\alpha : (X,R) \sqcup_{(E,R|_E)} (X,R) \to (Y,S),$$
-      and it remains to prove that $\alpha$ is relation-reflecting. By the construction of colimits, the pushout is given by
-      $$(X \sqcup_E X, i_1(R) \cup i_2(R)),$$
-      where $i_k(R)$ is shorthand for $\{(i_k(x),i_k(x')) : (x,x') \in R\}$. Thus, we need to show that for all elements $p,q \in X \sqcup_E X$ with $(\alpha(p),\alpha(q)) \in S$, we have $(p,q) \in i_1(R) \cup i_2(R)$. Since $p$ and $q$ are contained in $i_1(X) \cup i_2(X)$, there are four cases to consider.
-
-      <strong>Case 1.</strong> We have $p = i_1(x)$ and $q = i_1(x')$. Thus,
-      $$(q_1(x),q_1(x')) = (\alpha(p),\alpha(q)) \in S.$$
-      Applying the retraction $r : (Y,S) \to (X,R)$, we obtain $(x,x') \in R$. Thus,
-      $$(p,q) = (i_1(x),i_1(x')) \in i_1(R) \subseteq i_1(R) \cup i_2(R).$$
-      <strong>Case 2.</strong> We have $p = i_2(x)$ and $q = i_2(x')$. This is symmetric to Case 1.
-
-      <strong>Case 3.</strong> We have $p = i_1(x)$ and $q = i_2(x')$. Thus,
-      $$(q_1(x),q_2(x')) = (\alpha(p),\alpha(q)) \in S.$$
-      Consider the set
-      $$Z \coloneqq X \sqcup_E X \sqcup_E X.$$
-      There are three canonical injective maps
-      $$u_i : X \to Z$$
-      satisfying $u_i(x) = u_j(x') \iff x = x' \in E$ for $i \neq j$. Because $(u_1)|_E = (u_2)|_E$, there is a unique map $f : Y \to Z$ with $f q_1 = u_1$ and $f q_2 = u_2$. Likewise, there is a unique map $g : Y \to Z$ with $g q_1 = u_2$ and $g q_2 = u_3$. Consider the binary relation $T \coloneqq f(S) \cup g(S)$ on $Z$. Then $f$ and $g$ induce morphisms $f,g : (Y,S) \rightrightarrows (Z,T)$ satisfying $f q_2 = g q_1$. Since $q_1,q_2$ is cotransitive, there is a morphism
-      $$h : (Y,S) \to (Z,T)$$
-      satisfying $h q_1 = f q_1 = u_1$ and $h q_2 = g q_2 = u_3$. Since $(q_1(x),q_2(x')) \in S$ and $h$ is a morphism, we have
-      $$(u_1(x),u_3(x')) \in T = f(S) \cup g(S).$$
-      Assume first that $(u_1(x),u_3(x')) \in f(S)$. Then
-      $$u_3(x') \in \im(f) \subseteq \im(u_1) \cup \im(u_2),$$
-      so that $x' \in E$. But then $p = i_1(x)$ and $q = i_1(x')$, so that we are in Case 1. Next, assume that $(u_1(x),u_3(x')) \in g(S)$. Then
-      $$u_1(x) \in \im(g) \subseteq \im(u_2) \cup \im(u_3),$$
-      so that $x \in E$. But then $p = i_2(x)$ and $q = i_2(x')$, so that we are in Case 2.
-
-      <strong>Case 4.</strong> We have $p = i_2(x)$ and $q = i_1(x')$. This is symmetric to Case 3.
-
 unsatisfied_properties:
   - property: skeletal
     proof: This is trivial.

database/data/categories/Bin_refl.yaml

@@ -99,9 +99,6 @@ satisfied_properties:
     references:
       - Bin_extremal_cogenerator
 
-  - property: effective cocongruences
-    proof: This follows from the corresponding fact for <a href="/category/Bin">$\Bin$</a> and the dual of Lemma 8 <a href="/content/subcategories">here</a>.
-
 unsatisfied_properties:
   - property: skeletal
     proof: This is trivial.

database/data/categories/Bin_symm.yaml

@@ -86,9 +86,6 @@ satisfied_properties:
     references:
       - Bin_extremal_cogenerator
 
-  - property: effective cocongruences
-    proof: This follows from the corresponding fact for <a href="/category/Bin">$\Bin$</a> and the dual of Lemma 8 <a href="/content/subcategories">here</a>.
-
 unsatisfied_properties:
   - property: skeletal
     proof: This is trivial.

database/data/categories/Bin_symm_refl.yaml

@@ -87,9 +87,6 @@ satisfied_properties:
     references:
       - Bin_extremal_cogenerator
 
-  - property: effective cocongruences
-    proof: This follows from the corresponding fact for <a href="/category/Bin">$\Bin$</a> and the dual of Lemma 8 <a href="/content/subcategories">here</a>.
-
 unsatisfied_properties:
   - property: skeletal
     proof: This is trivial.

database/data/categories/Cat.yaml

@@ -45,9 +45,6 @@ unsatisfied_properties:
   - property: balanced
     proof: Since we know that <a href="/category/Mon">$\Mon$</a> is not balanced, there is a monoid map $M \to N$ which is a monomorphism and an epimorphism, but not an isomorphism. Then $B(M) \to B(N)$ has the corresponding properties.
 
-  - property: regular
-    proof: See Example 3.14 at the <a href="https://ncatlab.org/nlab/show/regular+category">nLab</a>.
-
   - property: coregular
     proof: 'We already know that <a href="/category/Mon">$\Mon$</a> is not coregular; in fact we have shown that there is a regular monomorphism $M \to N$ of monoids and a morphism $M \to K$ such that $K \to K \sqcup_M N$ is not a monomorphism. The delooping functor $B : \Mon \to \Cat$ has a left adjoint (<a href="https://math.stackexchange.com/questions/574745">MSE/574745</a>), hence it preserves regular monomorphisms. It also preserves pushouts (<a href="https://math.stackexchange.com/questions/5130854">MSE/5130854</a>), and it reflects monomorphisms since it is faithful. Therefore, $B(M) \to B(N)$ provides the desired counterexample of a non-stable regular monomorphism of categories.'
     references:

database/data/categories/LRS_R.yaml

@@ -88,9 +88,6 @@ unsatisfied_properties:
   - property: cartesian filtered colimits
     proof: This is Corollary 4(b) <a href="/content/Top-embeds-in-LRS">here</a>.
 
-  - property: regular
-    proof: This is Corollary 4(c) <a href="/content/Top-embeds-in-LRS">here</a>.
-
   - property: cofiltered-limit-stable epimorphisms
     proof: This is Corollary 4(d) <a href="/content/Top-embeds-in-LRS">here</a>.
 

database/data/categories/Meas.yaml

@@ -126,24 +126,6 @@ unsatisfied_properties:
     references:
       - Top_no_effective_cocongruences
 
-  - property: regular
-    proof: >-
-      In a regular category, regular epimorphisms are stable under pullbacks and compositions (see Prop. 3.7 at the <a href="https://ncatlab.org/nlab/show/regular+epimorphism">nLab</a>), which implies that for every regular epimorphism $f : X \to Y$ also $f \times f : X \times X \to Y \times Y$ is a regular epimorphism. We will show that this fails in $\Meas$.
-
-      Let $X \coloneqq [0, 1)$ equipped with the standard Borel $\sigma$-algebra $\B$. Consider the equivalence relation $x \sim y \iff x-y \in \IQ$, let $Y \coloneqq X /{\sim}$ be the set of equivalence classes, and $f: X \to Y$ be the natural projection map. Equip $Y$ with the quotient $\sigma$-algebra $\Sigma_Y$, so that $f$ is a regular epimorphism.
-
-      Now consider the diagonal in the quotient space $\Delta_Y \coloneqq \{(y, y) \mid y \in Y\}$. Then
-      $$\textstyle (f \times f)^{-1}(\Delta_Y) = \{(x_1, x_2) \in [0, 1)^2 \mid x_1 - x_2  \in \IQ\} \eqqcolon \bigcup_{q \in \IQ} L_q$$
-      where each $L_q$ is the intersection of the diagonal level sets of $x_1 - x_2$ with $[0, 1)^2$. Because each line is closed in $\IR^2$, its intersection with $[0, 1)^2$ is a Borel set in $X \times X$. Since a countable union of Borel sets is Borel, $(f \times f)^{-1}(\Delta_Y) \in \B \otimes \B$.
-
-      Now take any set $B \in \Sigma_Y$. Its preimage $f^{-1}(B)$ is a Borel set in $[0, 1)$ that is invariant under rational translations modulo 1. Because the action of $\IQ / \IZ$ on $[0, 1)$ is ergodic, the Lebesgue measure $\lambda(f^{-1}(B))$ must be exactly $0$ or $1$. Assume for contradiction that $\Sigma_Y$ is countably separated, i.e. there exists a countable sequence of measurable sets $(B_n)_{n \geq 1}$ in $\Sigma_Y$ that separates the points of $Y$. Let $A_n \coloneqq f^{-1}(B_n)$. Every $A_n$ has $\lambda(A_n) = 0$ or $\lambda(A_n) = 1$.
-
-      Define a "bad set" $N \subseteq [0, 1)$ as
-      $$\textstyle N \coloneqq \left( \bigcup_{\lambda(A_n)=0} A_n \right) \cup \left( \bigcup_{\lambda(A_n)=1} A_n^c \right)$$
-      Because $N$ is a countable union of sets with measure $0$, we have $\lambda(N) = 0$, and thus $\lambda([0, 1) \setminus N)=1$. For any two points $x, y \in [0, 1) \setminus N$, clearly $x \in A_n \iff y \in A_n$ for every $n$. Consequently, the sequence $(B_n)$ fails to separate $f(x)$ and $f(y)$. Hence, $x \sim y$. Since $[0, 1) \setminus N$ has measure $1$, it is uncountable. Because each equivalence class is only countable, these uncountably many points must belong to uncountably many different equivalence classes. Thus, we can easily pick $x, y \in [0, 1) \setminus N$ where $x \not\sim y$. Thus $\Sigma_Y$ is not countably separated.
-
-      Hence by <a href="https://link.springer.com/book/10.1007/978-3-540-34514-5">Bogachev</a>, Theorem 6.5.7, $\Delta_Y \notin \Sigma_Y \otimes \Sigma_Y$. We have identified a non-measurable subset of $Y \times Y$ whose preimage under $f \times f$ is measurable. Therefore, $f \times f$ is not a regular epimorphism.
-
   - property: extremal generating collection
     proof: >-
       The proof is similar to the one for <a href="/category/Top">$\Top$</a>. In this case, suppose $\kappa$ is an uncountable regular cardinal. We can then define $\M_\kappa$ to be the collection of subsets $E \subseteq \kappa + 1$ such that there exists an ordinal $\alpha < \kappa$ such that for each $\beta \in [\alpha, \kappa)$, $\beta \in E$ if and only if $\kappa \in E$. This is easily checked to be a $\sigma$-algebra on $\kappa + 1$. Similarly, define $\M_\kappa'$ to be the $\sigma$-algebra generated by $\M_\kappa \cup \{ \{ \kappa \} \}$; this can be described as the set of $E \subseteq \kappa + 1$ such that there exists an ordinal $\alpha < \kappa$ such that for each $\beta, \gamma \in [\alpha, \kappa)$, $\beta \in E$ if and only if $\gamma \in E$.

database/data/categories/Met_oo.yaml

@@ -70,11 +70,6 @@ unsatisfied_properties:
     references:
       - Met_no_effective_cocongruences
 
-  - property: regular
-    proof: We can take the same counterexample as for <a href="/category/PMet">$\PMet$</a>.
-    references:
-      - PMet_not_regular
-
   - property: regular subobject classifier
     proof: The same proof as for <a href="/category/Met">$\Met$</a> works.
     references:

database/data/categories/Mono.yaml

@@ -91,6 +91,7 @@ satisfied_properties:
 
   - property: effective cocongruences
     proof: 'See the proof that $\Mono$ is co-Malcev: It shows that in fact any coreflexive corelation is equivalent to an effective cocongruence $X \sqcup X \twoheadrightarrow X \sqcup_Y X$.'
+    check_redundancy: false
 
 unsatisfied_properties:
   - property: skeletal

database/data/categories/Pos.yaml

@@ -58,9 +58,6 @@ unsatisfied_properties:
   - property: balanced
     proof: The inclusion $\{0,1\} \to \{0 < 1\}$ provides a counterexample (where in the domain there is no relation between $0$ and $1$).
 
-  - property: regular
-    proof: See Example 3.14 at the <a href="https://ncatlab.org/nlab/show/regular+category">nLab</a>.
-
   - property: Malcev
     proof: 'Consider the subposet $\{(a,b) : a \leq b \}$ of $\IN^2$.'
 

database/data/categories/PreOrd.yaml

@@ -56,9 +56,6 @@ satisfied_properties:
       Finally, by <a href="/content/generator_construction">this result</a>, we can conclude that the product of $\{0,1\}_c$ and $\{0<1\}$ is an extremal cogenerator.
 
 unsatisfied_properties:
-  - property: regular
-    proof: See Example 3.14 at the <a href="https://ncatlab.org/nlab/show/regular+category">nLab</a>.
-
   - property: skeletal
     proof: This is trivial.
 

database/data/categories/Set_family_mostly_0.yaml

@@ -74,12 +74,6 @@ satisfied_properties:
   - property: effective congruences
     proof: Let $R \rightrightarrows X$ be a congruence in $\Set^{(I)}_0$. We claim that it is the kernel pair of its coequalizer $X \twoheadrightarrow X/R$. This certainly holds in <a href="/category/Set">$\Set$</a>, and for every $i \in I$, the pair $R_i \rightrightarrows X_i$ is a congruence in $\Set$. Therefore, the claim follows since kernel pairs (in fact, all connected limits) and coequalizers (in fact, all colimits) are constructed pointwise.
 
-  - property: effective cocongruences
-    proof: Let $X \rightrightarrows R$ be a cocongruence in $\Set^{(I)}_0$. We claim that it is the cokernel pair of its equalizer $E \hookrightarrow X$. This certainly holds in <a href="/category/Set">$\Set$</a>, and for every $i \in I$, the pair $X_i \rightrightarrows R_i$ is a cocongruence in $\Set$. Therefore, the claim follows since cokernel pairs (in fact, all colimits) and equalizers (in fact, all connected limits) are constructed pointwise.
-
-  - property: co-Malcev
-    proof: Since colimits are constructed pointwise, this property is inherited from <a href="/category/Set">$\Set$</a>.
-
 unsatisfied_properties:
   - property: skeletal
     proof: This is trivial.