Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 0 additions & 9 deletions databases/catdat/data/category-implications/algebraic.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -24,15 +24,6 @@
reason: The regular epimorphisms are precisely the sort-wise surjective homomorphisms, which are clearly stable under pullbacks.
is_equivalence: false

- id: algebras_with_0_disjoint_products
assumptions:
- finitary algebraic
- pointed
conclusions:
- disjoint products
reason: 'We have a constant in every algebra, let us denoted it by $0$. Then the projection $A \times B \to A$ is clearly surjective, hence an epimorphism. To show that $A \sqcup_{A \times B} B$ is trivial, let $R$ be an algebra which admits homomorphisms $f : A \to R$, $g : B \to R$ such that $f(p_1(a,b)) = g(p_2(a,b))$ for all $(a,b) \times A \times B$. This means $f(a) = g(b)$. In particular, $f(a) = g(0) = 0$. Likewise, $g(b) = 0$, and we are done.'
is_equivalence: false

- id: generalized_variety_require_sifted_colimit
assumptions:
- generalized variety
Expand Down
9 changes: 1 addition & 8 deletions databases/catdat/data/category-implications/thin.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -7,16 +7,9 @@
- generating set
- locally essentially small
- one-way
reason: This is trivial. The empty set is generating.
is_equivalence: false

- id: thin_consequence
assumptions:
- thin
conclusions:
- equalizers
- left cancellative
reason: Any two parallel morphisms are equal, so their equalizer is the identity, and every morphism is a monomorphism as well.
reason: This is trivial.
is_equivalence: false

- id: thin_inhabited_consequence
Expand Down
2 changes: 1 addition & 1 deletion src/components/Selection.svelte
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
<script lang="ts">
import ChipGroup from './ChipGroup.svelte'
import Chip from './Chip.svelte'
import { get_comparison_score, normalize_text } from '$lib/client/utils'
import { get_comparison_score } from '$lib/client/utils'

type Props = {
title?: string
Expand Down
2 changes: 1 addition & 1 deletion src/routes/category/[id]/+page.svelte
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
import TextWithReason from '$components/TextWithReason.svelte'
import { filter_by_tag, pluralize } from '$lib/client/utils'
import CategoryList from '$components/CategoryList.svelte'
import { faQuestion, faQuestionCircle } from '@fortawesome/free-solid-svg-icons'
import { faQuestion } from '@fortawesome/free-solid-svg-icons'
import Fa from 'svelte-fa'
import SuggestionForm from '$components/SuggestionForm.svelte'

Expand Down
2 changes: 1 addition & 1 deletion src/routes/functor-search/+page.server.ts
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ import { query } from '$lib/server/db.catdat'
import { error } from '@sveltejs/kit'
import sql from 'sql-template-tag'

export const load = async (event) => {
export const load = async () => {
const { rows, err } = query<{ id: string }>(sql`
SELECT id FROM functor_properties ORDER BY lower(id)
`)
Expand Down
2 changes: 1 addition & 1 deletion src/routes/lemma/[id]/+page.server.ts
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import type { CategoryShort, Lemma } from '$lib/commons/types'
import { batch, query } from '$lib/server/db.catdat'
import { batch } from '$lib/server/db.catdat'
import { render_nested_formulas } from '$lib/server/rendering'
import { error } from '@sveltejs/kit'
import sql from 'sql-template-tag'
Expand Down
3 changes: 1 addition & 2 deletions src/routes/lemmas/+page.server.ts
Original file line number Diff line number Diff line change
@@ -1,10 +1,9 @@
import type { Lemma } from '$lib/commons/types'
import { query } from '$lib/server/db.catdat'
import { render_nested_formulas } from '$lib/server/rendering'
import { error } from '@sveltejs/kit'
import sql from 'sql-template-tag'

export const load = async (event) => {
export const load = async () => {
const { rows: lemmas, err } = query<Lemma>(
sql`SELECT id, title, claim, proof FROM lemmas ORDER BY lower(title)`,
)
Expand Down
4 changes: 3 additions & 1 deletion tsconfig.json
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,9 @@
"skipLibCheck": true,
"sourceMap": true,
"strict": true,
"moduleResolution": "bundler"
"moduleResolution": "bundler",
"noUnusedLocals": true,
"noUnusedParameters": true
}
// Path aliases are handled by https://svelte.dev/docs/kit/configuration#alias
// except $lib which is handled by https://svelte.dev/docs/kit/configuration#files
Expand Down