From e13f6afc590657b1a13f548da9292507897bc635 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 18 May 2026 22:44:00 +0200 Subject: [PATCH 01/26] merge CategoryList and FunctorList into one component --- src/components/CategoryList.svelte | 36 ------------------ src/components/EntityList.svelte | 37 ++++++++++++++++++ src/components/FunctorList.svelte | 38 ------------------- src/lib/commons/types.ts | 5 +++ src/routes/categories/+page.svelte | 4 +- src/routes/categories/[tag]/+page.svelte | 4 +- .../category-implication/[id]/+page.svelte | 4 +- .../category-property/[id]/+page.svelte | 8 ++-- .../category-search/results/+page.svelte | 4 +- src/routes/category/[id]/+page.svelte | 4 +- src/routes/content/[id]/+page.svelte | 4 +- .../functor-implication/[id]/+page.svelte | 4 +- src/routes/functor-property/[id]/+page.svelte | 8 ++-- .../functor-search/results/+page.svelte | 4 +- src/routes/functors/+page.svelte | 4 +- src/routes/missing/+page.svelte | 9 ++--- 16 files changed, 72 insertions(+), 105 deletions(-) delete mode 100644 src/components/CategoryList.svelte create mode 100644 src/components/EntityList.svelte delete mode 100644 src/components/FunctorList.svelte diff --git a/src/components/CategoryList.svelte b/src/components/CategoryList.svelte deleted file mode 100644 index 13820daf..00000000 --- a/src/components/CategoryList.svelte +++ /dev/null @@ -1,36 +0,0 @@ - - -{#if categories.length} - -{:else} -

—

-{/if} - - diff --git a/src/components/EntityList.svelte b/src/components/EntityList.svelte new file mode 100644 index 00000000..5b3eb8e9 --- /dev/null +++ b/src/components/EntityList.svelte @@ -0,0 +1,37 @@ + + +{#if entities.length} + +{:else} +

—

+{/if} + + diff --git a/src/components/FunctorList.svelte b/src/components/FunctorList.svelte deleted file mode 100644 index 851e6d0d..00000000 --- a/src/components/FunctorList.svelte +++ /dev/null @@ -1,38 +0,0 @@ - - -{#if functors.length} - -{:else} -

—

-{/if} - - diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index bed2e1ef..185160ce 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -17,6 +17,11 @@ export type CategoryDisplay = { dual_category_notation: string | null } +export type EntityShort = { + id: string + name: string +} + export type CategoryShort = Pick export type RelatedCategory = Pick diff --git a/src/routes/categories/+page.svelte b/src/routes/categories/+page.svelte index 789df806..be456e46 100644 --- a/src/routes/categories/+page.svelte +++ b/src/routes/categories/+page.svelte @@ -1,11 +1,11 @@ diff --git a/src/components/CategoryImplicationList.svelte b/src/components/CategoryImplicationList.svelte index b1151447..daa90c3e 100644 --- a/src/components/CategoryImplicationList.svelte +++ b/src/components/CategoryImplicationList.svelte @@ -1,9 +1,9 @@ - - - - - -{#each implication.assumptions as assumption, i} - {assumption} - {#if i < implication.assumptions.length - 1} - - - {/if} -{/each} - - - - - -{#each implication.conclusions as conclusion, i} - {conclusion} - {#if i < implication.conclusions.length - 1} - - - {/if} -{/each} - - diff --git a/src/components/CategoryImplicationList.svelte b/src/components/CategoryImplicationList.svelte deleted file mode 100644 index daa90c3e..00000000 --- a/src/components/CategoryImplicationList.svelte +++ /dev/null @@ -1,23 +0,0 @@ - - -{#if implications.length} -
    - {#each implications as implication} -
  • - -
    • - {/each} -
-{:else} -

—

-{/if} diff --git a/src/components/FunctorImplicationList.svelte b/src/components/FunctorImplicationList.svelte deleted file mode 100644 index fcdc5eb1..00000000 --- a/src/components/FunctorImplicationList.svelte +++ /dev/null @@ -1,29 +0,0 @@ - - -{#if implications.length} -
    - {#each implications as implication} -
  • - -
    • - {/each} -
- -

- *Those implications also require assumptions on the source or target category. -

-{:else} -

—

-{/if} diff --git a/src/components/FunctorImplicationItem.svelte b/src/components/ImplicationItem.svelte similarity index 76% rename from src/components/FunctorImplicationItem.svelte rename to src/components/ImplicationItem.svelte index 953a03d5..5d753989 100644 --- a/src/components/FunctorImplicationItem.svelte +++ b/src/components/ImplicationItem.svelte @@ -1,6 +1,4 @@ - + {#each implication.assumptions as assumption, i} {assumption} {#if i < implication.assumptions.length - 1} @@ -54,7 +53,7 @@ {#each implication.conclusions as conclusion, i} {conclusion} {#if i < implication.conclusions.length - 1} @@ -62,7 +61,8 @@ {/if} {/each} -{#if implication.source_assumptions.length > 0 || implication.target_assumptions.length > 0} + +{#if implication.source_assumptions?.length || implication.target_assumptions?.length} * {/if} diff --git a/src/components/ImplicationList.svelte b/src/components/ImplicationList.svelte new file mode 100644 index 00000000..485de823 --- /dev/null +++ b/src/components/ImplicationList.svelte @@ -0,0 +1,30 @@ + + +{#if implications.length} +
    + {#each implications as implication} +
  • + +
    • + {/each} +
+ + {#if type === 'functor'} +

+ *Those implications also require assumptions on the source or target category. +

+ {/if} +{:else} +

—

+{/if} diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index a55b3edf..cd810e31 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -28,7 +28,6 @@ export type TagObject = { tag: string } export type CommentObject = { id: number; comment: string } -// used for both categories and functors export type PropertyDB = { id: string relation: string @@ -84,7 +83,7 @@ export type FunctorDB = { nlab_link: string | null } -export type CategoryImplicationDB = { +export type ImplicationDB = { id: string is_equivalence: 0 | 1 is_deduced: 0 | 1 @@ -92,38 +91,18 @@ export type CategoryImplicationDB = { reason: string assumptions: string conclusions: string + source_assumptions?: string // for functors + target_assumptions?: string // for functors } -export type FunctorImplicationDB = { - id: string - is_equivalence: 0 | 1 - is_deduced: 0 | 1 - dualized_from: string | null - reason: string - assumptions: string - conclusions: string - source_assumptions: string - target_assumptions: string -} - -export type FunctorImplicationDisplay = Replace< - FunctorImplicationDB, - { - is_equivalence: boolean - is_deduced: boolean - assumptions: string[] - conclusions: string[] - source_assumptions: string[] - target_assumptions: string[] - } -> - -export type CategoryImplicationDisplay = Replace< - CategoryImplicationDB, +export type ImplicationDisplay = Replace< + ImplicationDB, { is_equivalence: boolean is_deduced: boolean assumptions: string[] conclusions: string[] + source_assumptions?: string[] + target_assumptions?: string[] } > diff --git a/src/lib/server/transforms.ts b/src/lib/server/transforms.ts index f83cf65e..dbb08a07 100644 --- a/src/lib/server/transforms.ts +++ b/src/lib/server/transforms.ts @@ -1,15 +1,12 @@ import type { - FunctorImplicationDB, - FunctorImplicationDisplay, - CategoryImplicationDB, - CategoryImplicationDisplay, PropertyDB, PropertyDisplay, PropertyAssignmentDB, PropertyAssignmentDisplay, + ImplicationDB, + ImplicationDisplay, } from '$lib/commons/types' -// this function is used for both categories and functors export function display_property(property: PropertyDB): PropertyDisplay { return { id: property.id, @@ -32,9 +29,7 @@ export function display_property_assignment( } } -export function display_implication( - implication: CategoryImplicationDB, -): CategoryImplicationDisplay { +export function display_implication(implication: ImplicationDB): ImplicationDisplay { return { id: implication.id, is_equivalence: Boolean(implication.is_equivalence), @@ -42,22 +37,12 @@ export function display_implication( dualized_from: implication.dualized_from, reason: implication.reason, assumptions: JSON.parse(implication.assumptions), - conclusions: JSON.parse(implication.conclusions), - } -} - -export function display_functor_implication( - implication: FunctorImplicationDB, -): FunctorImplicationDisplay { - return { - id: implication.id, - is_equivalence: Boolean(implication.is_equivalence), - is_deduced: Boolean(implication.is_deduced), - dualized_from: implication.dualized_from, - reason: implication.reason, - assumptions: JSON.parse(implication.assumptions), - source_assumptions: JSON.parse(implication.source_assumptions), - target_assumptions: JSON.parse(implication.target_assumptions), + source_assumptions: implication.source_assumptions + ? JSON.parse(implication.source_assumptions) + : undefined, + target_assumptions: implication.target_assumptions + ? JSON.parse(implication.target_assumptions) + : undefined, conclusions: JSON.parse(implication.conclusions), } } diff --git a/src/routes/category-implication/[id]/+page.server.ts b/src/routes/category-implication/[id]/+page.server.ts index f809613f..cd93cc71 100644 --- a/src/routes/category-implication/[id]/+page.server.ts +++ b/src/routes/category-implication/[id]/+page.server.ts @@ -1,4 +1,4 @@ -import type { EntityShort, CategoryImplicationDB } from '$lib/commons/types' +import type { EntityShort, ImplicationDB } 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/transforms' @@ -8,7 +8,7 @@ import sql from 'sql-template-tag' export const load = async (event) => { const id = event.params.id - const { results, err } = batch<[CategoryImplicationDB, EntityShort]>([ + const { results, err } = batch<[ImplicationDB, EntityShort]>([ sql` SELECT id, diff --git a/src/routes/category-implications/+page.server.ts b/src/routes/category-implications/+page.server.ts index 71a08a40..7df454d4 100644 --- a/src/routes/category-implications/+page.server.ts +++ b/src/routes/category-implications/+page.server.ts @@ -2,11 +2,11 @@ import { render_nested_formulas } from '$lib/server/formulas' import { query } from '$lib/server/db.catdat' import sql from 'sql-template-tag' import { error } from '@sveltejs/kit' -import type { CategoryImplicationDB } from '$lib/commons/types' +import type { ImplicationDB } from '$lib/commons/types' import { display_implication } from '$lib/server/transforms' export const load = async () => { - const { rows, err } = query(sql` + const { rows, err } = query(sql` SELECT id, is_equivalence, diff --git a/src/routes/category-implications/+page.svelte b/src/routes/category-implications/+page.svelte index 02acfe9f..21cb5bfa 100644 --- a/src/routes/category-implications/+page.svelte +++ b/src/routes/category-implications/+page.svelte @@ -1,7 +1,7 @@ - -{#if entities.length} -
    - {#each entities as entity} -
  • - - {entity.name} - - {#if entity.count !== undefined} - ({entity.count}) - {/if} -
    • - {/each} -
-{:else} -

—

-{/if} - - diff --git a/src/components/Header.svelte b/src/components/Header.svelte index 578700de..63777e94 100644 --- a/src/components/Header.svelte +++ b/src/components/Header.svelte @@ -2,14 +2,14 @@ import { faBars } from '@fortawesome/free-solid-svg-icons' import Fa from 'svelte-fa' import StructureSelector from './StructureSelector.svelte' - import type { Structure } from '$lib/commons/types' + import type { StructureType } from '$lib/commons/types' type Props = { open_mobile_nav: () => void - structure: Structure + selected_type: StructureType } - let { open_mobile_nav, structure }: Props = $props() + let { open_mobile_nav, selected_type }: Props = $props()
@@ -33,7 +33,7 @@
- +
- - - - - + can look for categories that are finitely complete and pointed + but not complete. + diff --git a/src/routes/category-search/results/+page.svelte b/src/routes/category-search/results/+page.svelte index 96ea96e7..b0b14042 100644 --- a/src/routes/category-search/results/+page.svelte +++ b/src/routes/category-search/results/+page.svelte @@ -1,100 +1,6 @@ - - -

Search Results

- -{#if data.satisfied_properties.length > 0} -
- Satisfied properties: - - {#each data.satisfied_properties as property, index} - {property}{#if index < data.satisfied_properties.length - 1} - ,  - {/if} - {/each} -
-{/if} - -{#if data.unsatisfied_properties.length > 0} -
- Unsatisfied properties: - - {#each data.unsatisfied_properties as property, index} - {property}{#if index < data.unsatisfied_properties.length - 1} - ,  - {/if} - {/each} -
-{/if} - -{#if !data.contradiction} -

- {pluralize(data.found_structures.length, { - one: 'Found {count} category', - other: 'Found {count} categories', - })} -

- -{:else} -

- No categories found because the requirements are inconsistent: -

- -
    - {#each data.contradiction as segment} -
  1. {segment}
    2. - {/each} -
-{/if} - - - Adjust search - - {#if data.dual_search_available} - Dualize search - {/if} - - - + diff --git a/src/routes/functor-search/+page.server.ts b/src/routes/functor-search/+page.server.ts index 47313e34..bc77cc3f 100644 --- a/src/routes/functor-search/+page.server.ts +++ b/src/routes/functor-search/+page.server.ts @@ -1,15 +1,5 @@ -import { query } from '$lib/server/db.catdat' -import { error } from '@sveltejs/kit' -import sql from 'sql-template-tag' +import { get_property_ids } from '$lib/server/properties' export const load = async () => { - const { rows, err } = query<{ id: string }>(sql` - SELECT id FROM functor_properties ORDER BY lower(id) - `) - - if (err) error(500, 'Failed to load properties') - - const all_properties = rows.map(({ id }) => id) - - return { all_properties } + return { all_properties: get_property_ids('functor') } } diff --git a/src/routes/functor-search/+page.svelte b/src/routes/functor-search/+page.svelte index a722776f..cbf217ef 100644 --- a/src/routes/functor-search/+page.svelte +++ b/src/routes/functor-search/+page.svelte @@ -1,127 +1,12 @@ - - -

Property combo search

- -

+ Search for functors with certain properties while excluding others. For example, you - can look - for functors that are continuous but not cocontinuous. -

- - - - - - - - - - - - + can look for functors that are continuous but not cocontinuous. + diff --git a/src/routes/functor-search/results/+page.svelte b/src/routes/functor-search/results/+page.svelte index 76f1ef0c..b0b14042 100644 --- a/src/routes/functor-search/results/+page.svelte +++ b/src/routes/functor-search/results/+page.svelte @@ -1,101 +1,6 @@ - - -

Search results

- -{#if data.satisfied_properties.length > 0} -
- Satisfied properties: - - {#each data.satisfied_properties as property, index} - {property}{#if index < data.satisfied_properties.length - 1} - ,  - {/if} - {/each} -
-{/if} - -{#if data.unsatisfied_properties.length > 0} -
- Unsatisfied properties: - - {#each data.unsatisfied_properties as property, index} - {property}{#if index < data.unsatisfied_properties.length - 1} - ,  - {/if} - {/each} -
-{/if} - -{#if !data.contradiction} -

- {pluralize(data.found_structures.length, { - one: 'Found {count} functor', - other: 'Found {count} functors', - })} -

- - -{:else} -

- No functors found because the requirements are inconsistent: -

- -
    - {#each data.contradiction as segment} -
  1. {segment}
    2. - {/each} -
-{/if} - - - Adjust search - - {#if data.dual_search_available} - Dualize search - {/if} - - - + diff --git a/svelte.config.js b/svelte.config.js index 34786a4d..6fab18a7 100644 --- a/svelte.config.js +++ b/svelte.config.js @@ -7,6 +7,7 @@ const config = { kit: { alias: { $components: './src/components', + $pages: './src/pages', }, adapter: adapter(), }, From af83585deff097032aeca84a4e7eaffa69403d33 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 24 May 2026 09:29:01 +0200 Subject: [PATCH 11/26] unify implication pages --- src/components/ImplicationItem.svelte | 53 ++++---- src/components/ImplicationList.svelte | 6 - src/pages/ImplicationListPage.svelte | 80 +++++++++++++ src/pages/ImplicationPage.svelte | 113 ++++++++++++++++++ .../category-implication/[id]/+page.svelte | 76 +----------- src/routes/category-implications/+page.svelte | 109 ++++------------- .../functor-implication/[id]/+page.svelte | 103 ++-------------- src/routes/functor-implications/+page.svelte | 37 +++--- 8 files changed, 281 insertions(+), 296 deletions(-) create mode 100644 src/pages/ImplicationListPage.svelte create mode 100644 src/pages/ImplicationPage.svelte diff --git a/src/components/ImplicationItem.svelte b/src/components/ImplicationItem.svelte index 13307c61..b66cdf16 100644 --- a/src/components/ImplicationItem.svelte +++ b/src/components/ImplicationItem.svelte @@ -10,12 +10,17 @@ import type { ImplicationDisplay, StructureType } from '$lib/commons/types' type Props = { + type: StructureType implication: ImplicationDisplay highlighted_property?: string - type: StructureType } - let { implication, highlighted_property, type }: Props = $props() + let { type, implication, highlighted_property }: Props = $props() + + let has_additional_assumptions = $derived( + Boolean(implication.source_assumptions?.length) || + Boolean(implication.target_assumptions?.length), + ) @@ -26,19 +31,26 @@ {assumption} + {assumption} + + {#if i < implication.assumptions.length - 1} - - + + + + {/if} {/each} -