diff --git a/content/constant_morphisms.md b/content/constant_morphisms.md index 8962a069..d56815db 100644 --- a/content/constant_morphisms.md +++ b/content/constant_morphisms.md @@ -30,7 +30,7 @@ If $X$ is a subterminal object, then any morphism $X \to Y$ is constant. If $Y$ _Proof._ This is immediate from the definitions. $\square$ ::: Lemma 5 -If $f : X \to Y$ is a monomorphism that is constant, then $X$ is subterminal. +If $f : X \to Y$ is a monomorphism that is constant, then $X$ is subterminal. ::: _Proof._ If $x_1,x_2 : T \rightrightarrows X$ are morphisms, then $f \circ x_1 = f \circ x_2$ since $f$ is constant. Since $f$ is also a monomorphism, we infer that $x_1 = x_2$. $\square$ diff --git a/content/contribute.md b/content/contribute.md index 2f9b9cb1..8dd0b74e 100644 --- a/content/contribute.md +++ b/content/contribute.md @@ -5,7 +5,7 @@ description: CatDat welcomes contributions from the community, including filling ## How to contribute -_CatDat_ is developed in an open-source [GitHub repository](https://github.com/ScriptRaccoon/catdat) owned by [Martin Brandenburg](https://ncatlab.org/nlab/show/Martin+Brandenburg). It welcomes contributions from the community, including filling in missing information or discovering new combinations of properties. +_CatDat_ is developed in an open-source [GitHub repository](https://github.com/ScriptRaccoon/catdat) by [Martin Brandenburg](https://ncatlab.org/nlab/show/Martin+Brandenburg). It welcomes contributions from the community, including filling in missing information or discovering new combinations of properties. [**Video tutorial**](https://www.youtube.com/watch?v=NoZWdMFfQfg) diff --git a/content/sifted-colimits-in-groupoids.md b/content/sifted-colimits-in-groupoids.md index cc6c2530..0ec43ba6 100644 --- a/content/sifted-colimits-in-groupoids.md +++ b/content/sifted-colimits-in-groupoids.md @@ -55,7 +55,7 @@ $$h u_i = v_{i_0} D(b)^{-1} D(a) = v_k D(a) = v_i.$$ Moreover, $h$ is uniquely determined: if $v_i = h u_i$ for all $i \in \I$, then for $i = i_0$ we obtain $v_{i_0} = h$. $\square$ ::: Corollary 2 -Let $\C$ be a category with the property that every sifted diagram is eventually constant (for example, a groupoid). Then every object $X \in \C$ is strongly finitely presentable, i.e. the functor $\Hom(X,-) : \C \to \Set$ preserves sifted colimits. +Let $\C$ be a category with the property that every sifted diagram is eventually constant (for example, a groupoid). Then every object $X \in \C$ is strongly finitely presentable, i.e. the functor $\Hom(X,-) : \C \to \Set$ preserves sifted colimits. ::: _Proof._ diff --git a/src/components/Popup.svelte b/src/components/Popup.svelte index 4dcbebdd..ed78e1a3 100644 --- a/src/components/Popup.svelte +++ b/src/components/Popup.svelte @@ -88,7 +88,9 @@ an issue when clicking two proofs in a row. So it's a
+
Claim: {#if has_associated_assumptions} Given a {remove_underscores(type)} @@ -88,7 +88,7 @@ {/each}
-+
Proof: {@html implication.proof}
diff --git a/src/pages/PropertyPage.svelte b/src/pages/PropertyPage.svelte index 248a8d3c..4875c2e6 100644 --- a/src/pages/PropertyPage.svelte +++ b/src/pages/PropertyPage.svelte @@ -48,7 +48,7 @@+
{@html property.description} {#if property.invariant_under_equivalences === false} diff --git a/src/pages/StructureDetailPage.svelte b/src/pages/StructureDetailPage.svelte index 7cc8a2a8..d40ad071 100644 --- a/src/pages/StructureDetailPage.svelte +++ b/src/pages/StructureDetailPage.svelte @@ -134,7 +134,7 @@ {/if} -
{@html structure.description}
+{@html structure.description}