diff --git a/databases/catdat/data/category-implications/initial objects.yaml b/databases/catdat/data/category-implications/initial objects.yaml index 91a3c506..ec755d79 100644 --- a/databases/catdat/data/category-implications/initial objects.yaml +++ b/databases/catdat/data/category-implications/initial objects.yaml @@ -34,12 +34,3 @@ - strict initial object reason: 'It suffices to prove that in general any monomorphism $f : A \to 0$ into an initial object is an isomorphism. If $g : 0 \to A$ is the unique morphism, then $f \circ g = \id_0$ since $0$ is initial. But then $f$ is a split epimorphism and a monomorphism, hence an isomorphism.' is_equivalence: false - -- id: strict_initial_right_criterion - assumptions: - - initial object - - right cancellative - conclusions: - - strict initial object - reason: 'Let $f : A \to 0$ be a morphism. Let $g : 0 \to A$ be the unique morphism. It is an epimorphism by assumption. Also, $f \circ g = \id_0$ since $0$ is initial. But then $g$ is a split monomorphism and an epimorphism, hence an isomorphism.' - is_equivalence: false diff --git a/src/routes/app.css b/src/routes/app.css index 78ad0458..a91a6a64 100644 --- a/src/routes/app.css +++ b/src/routes/app.css @@ -111,6 +111,10 @@ p { margin-block: 1rem; } +details { + margin-block: 1rem; +} + a { color: inherit; text-underline-offset: 2px; diff --git a/src/routes/category-implication/[id]/+page.server.ts b/src/routes/category-implication/[id]/+page.server.ts index 8d72521a..de3769be 100644 --- a/src/routes/category-implication/[id]/+page.server.ts +++ b/src/routes/category-implication/[id]/+page.server.ts @@ -1,5 +1,5 @@ -import type { ImplicationDB, ImplicationDisplay } from '$lib/commons/types' -import { query } from '$lib/server/db.catdat' +import type { CategoryShort, ImplicationDB, ImplicationDisplay } from '$lib/commons/types' +import { batch } from '$lib/server/db.catdat' import { render_nested_formulas } from '$lib/server/formulas' import { display_implication } from '$lib/server/utils' import { error } from '@sveltejs/kit' @@ -8,24 +8,36 @@ import sql from 'sql-template-tag' export const load = async (event) => { const id = event.params.id - const { rows, err } = query(sql` - SELECT - id, - is_equivalence, - reason, - assumptions, - conclusions, - is_deduced, - dualized_from - FROM category_implications_view - WHERE id = ${id} - `) + const { results, err } = batch<[ImplicationDB, CategoryShort]>([ + sql` + SELECT + id, + is_equivalence, + reason, + assumptions, + conclusions, + is_deduced, + dualized_from + FROM category_implications_view + WHERE id = ${id} + `, + sql` + SELECT c.id, c.name FROM categories c + WHERE EXISTS ( + SELECT 1 FROM category_property_assignments cp + WHERE cp.category_id = c.id + AND cp.reason LIKE '%/category-implication/' || ${id} || '%' + ) + `, + ]) if (err) error(500, 'Could not load implication') - if (!rows.length) error(404, `Could not find implication with ID '${id}'`) + const [implications, categories] = results - const implication: ImplicationDisplay = display_implication(rows[0]) + if (!implications.length) error(404, `Could not find implication with ID '${id}'`) - return render_nested_formulas({ implication }) + const implication: ImplicationDisplay = display_implication(implications[0]) + + return render_nested_formulas({ implication, categories }) } diff --git a/src/routes/category-implication/[id]/+page.svelte b/src/routes/category-implication/[id]/+page.svelte index 1a202aad..eb40ce10 100644 --- a/src/routes/category-implication/[id]/+page.svelte +++ b/src/routes/category-implication/[id]/+page.svelte @@ -1,6 +1,8 @@