From d8ff6aa4b9e53d86b9b2eafbf20fc4d39ccbea64 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 21 Mar 2026 10:31:57 +0100 Subject: [PATCH 01/10] add tables for functors and their properties --- database/data/000_clear.sql | 11 +++ database/migrations/017_functors-table.sql | 11 +++ .../018_functor-properties-tables.sql | 22 +++++ .../migrations/019_functor-implications.sql | 54 +++++++++++++ .../020_functor-implication-view.sql | 80 +++++++++++++++++++ 5 files changed, 178 insertions(+) create mode 100644 database/migrations/017_functors-table.sql create mode 100644 database/migrations/018_functor-properties-tables.sql create mode 100644 database/migrations/019_functor-implications.sql create mode 100644 database/migrations/020_functor-implication-view.sql diff --git a/database/data/000_clear.sql b/database/data/000_clear.sql index b4ca547..bb8c4fd 100644 --- a/database/data/000_clear.sql +++ b/database/data/000_clear.sql @@ -21,6 +21,17 @@ DELETE FROM tags; DELETE FROM related_properties; DELETE FROM properties; + +DELETE FROM functor_property_assignments; +DELETE FROM functor_properties; +DELETE FROM functors; + DELETE FROM prefixes; +DELETE FROM functor_implication_assumptions; +DELETE FROM functor_implication_conclusions; +DELETE FROM functor_implication_source_assumptions; +DELETE FROM functor_implication_target_assumptions; +DELETE FROM functor_implications; + PRAGMA foreign_keys = ON; \ No newline at end of file diff --git a/database/migrations/017_functors-table.sql b/database/migrations/017_functors-table.sql new file mode 100644 index 0000000..21c24e9 --- /dev/null +++ b/database/migrations/017_functors-table.sql @@ -0,0 +1,11 @@ +CREATE TABLE functors ( + id TEXT PRIMARY KEY, + name TEXT NOT NULL UNIQUE, + source TEXT NOT NULL, + target TEXT NOT NULL, + description TEXT NOT NULL CHECK (length(description) > 0), + url TEXT CHECK (url IS NULL OR url like 'https://%'), + created_at TEXT NOT NULL DEFAULT CURRENT_TIMESTAMP, + FOREIGN KEY (source) REFERENCES categories (id) ON DELETE CASCADE, + FOREIGN KEY (target) REFERENCES categories (id) ON DELETE CASCADE +); \ No newline at end of file diff --git a/database/migrations/018_functor-properties-tables.sql b/database/migrations/018_functor-properties-tables.sql new file mode 100644 index 0000000..d5693d8 --- /dev/null +++ b/database/migrations/018_functor-properties-tables.sql @@ -0,0 +1,22 @@ +CREATE TABLE functor_properties ( + id TEXT PRIMARY KEY, + prefix TEXT NOT NULL, + description TEXT NOT NULL CHECK (length(description) > 0), + nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'), + invariant_under_equivalences INTEGER NOT NULL DEFAULT TRUE, + dual_property_id TEXT, + created_at TEXT NOT NULL DEFAULT CURRENT_TIMESTAMP, + FOREIGN KEY (prefix) REFERENCES prefixes (prefix) ON DELETE RESTRICT, + FOREIGN KEY (dual_property_id) REFERENCES functor_properties (id) ON DELETE SET NULL +); + +CREATE TABLE functor_property_assignments ( + functor_id TEXT NOT NULL, + property_id TEXT NOT NULL, + reason TEXT NOT NULL CHECK (length(reason) > 0), + is_satisfied INTEGER NOT NULL CHECK (is_satisfied IN (TRUE, FALSE)), + created_at TEXT NOT NULL DEFAULT CURRENT_TIMESTAMP, + PRIMARY KEY (functor_id, property_id), + FOREIGN KEY (functor_id) REFERENCES functors (id) ON DELETE CASCADE, + FOREIGN KEY (property_id) REFERENCES functor_properties (id) ON DELETE CASCADE +); \ No newline at end of file diff --git a/database/migrations/019_functor-implications.sql b/database/migrations/019_functor-implications.sql new file mode 100644 index 0000000..5c6c700 --- /dev/null +++ b/database/migrations/019_functor-implications.sql @@ -0,0 +1,54 @@ +CREATE TABLE functor_implications ( + id TEXT PRIMARY KEY, + reason TEXT NOT NULL CHECK (length(reason) > 0), + dualized_from TEXT, + is_equivalence INTEGER NOT NULL DEFAULT FALSE, + created_at TEXT NOT NULL DEFAULT CURRENT_TIMESTAMP, + FOREIGN KEY (dualized_from) REFERENCES functor_implications (id) ON DELETE SET NULL +); + +CREATE TABLE functor_implication_assumptions ( + implication_id TEXT NOT NULL, + property_id TEXT NOT NULL, + created_at TEXT NOT NULL DEFAULT CURRENT_TIMESTAMP, + PRIMARY KEY (implication_id, property_id), + FOREIGN KEY (implication_id) REFERENCES functor_implications (id) ON DELETE CASCADE, + FOREIGN KEY (property_id) REFERENCES functor_properties (id) ON DELETE CASCADE +); + +CREATE TABLE functor_implication_conclusions ( + implication_id TEXT NOT NULL, + property_id TEXT NOT NULL, + created_at TEXT NOT NULL DEFAULT CURRENT_TIMESTAMP, + PRIMARY KEY (implication_id, property_id), + FOREIGN KEY (implication_id) REFERENCES functor_implications (id) ON DELETE CASCADE, + FOREIGN KEY (property_id) REFERENCES functor_properties (id) ON DELETE CASCADE +); + +-- property of source category +CREATE TABLE functor_implication_source_assumptions ( + implication_id TEXT NOT NULL, + property_id TEXT NOT NULL, + created_at TEXT NOT NULL DEFAULT CURRENT_TIMESTAMP, + PRIMARY KEY (implication_id, property_id), + FOREIGN KEY (implication_id) REFERENCES functor_implications (id) ON DELETE CASCADE, + FOREIGN KEY (property_id) REFERENCES properties (id) ON DELETE CASCADE +); + +-- property of target category +CREATE TABLE functor_implication_target_assumptions ( + implication_id TEXT NOT NULL, + property_id TEXT NOT NULL, + created_at TEXT NOT NULL DEFAULT CURRENT_TIMESTAMP, + PRIMARY KEY (implication_id, property_id), + FOREIGN KEY (implication_id) REFERENCES functor_implications (id) ON DELETE CASCADE, + FOREIGN KEY (property_id) REFERENCES properties (id) ON DELETE CASCADE +); + +CREATE INDEX idx_assumptions_functor_property ON functor_implication_assumptions (property_id); + +CREATE INDEX idx_conclusions_functor_property ON functor_implication_conclusions (property_id); + +CREATE INDEX idx_assumptions_functor_source_property ON functor_implication_source_assumptions (property_id); + +CREATE INDEX idx_conclusions_functor_target_property ON functor_implication_target_assumptions (property_id); \ No newline at end of file diff --git a/database/migrations/020_functor-implication-view.sql b/database/migrations/020_functor-implication-view.sql new file mode 100644 index 0000000..76528ce --- /dev/null +++ b/database/migrations/020_functor-implication-view.sql @@ -0,0 +1,80 @@ +CREATE VIEW functor_implications_view AS +SELECT + i.id, + i.is_equivalence, + i.reason, + i.dualized_from, + ( + SELECT json_group_array(property_id) FROM ( + SELECT property_id + FROM functor_implication_assumptions a + WHERE a.implication_id = i.id + ORDER BY lower(property_id) + ) + ) AS assumptions, + ( + SELECT json_group_array(property_id) FROM ( + SELECT property_id + FROM functor_implication_source_assumptions a + WHERE a.implication_id = i.id + ORDER BY lower(property_id) + ) + ) AS source_assumptions, + ( + SELECT json_group_array(property_id) FROM ( + SELECT property_id + FROM functor_implication_target_assumptions a + WHERE a.implication_id = i.id + ORDER BY lower(property_id) + ) + ) AS target_assumptions, + ( + SELECT json_group_array(property_id) FROM ( + SELECT property_id + FROM functor_implication_conclusions c + WHERE c.implication_id = i.id + ORDER BY lower(property_id) + ) + ) AS conclusions +FROM functor_implications i; + + +CREATE VIEW functor_implication_input AS +SELECT + NULL AS id, + NULL AS is_equivalence, + NULL AS assumptions, + NULL AS source_assumptions, + NULL AS target_assumptions, + NULL AS conclusions, + NULL AS reason, + NULL AS dualized_from; + + +CREATE TRIGGER trg_functor_implication_input_insert +INSTEAD OF INSERT ON functor_implication_input +BEGIN + INSERT INTO functor_implications (id, reason, is_equivalence, dualized_from) + VALUES ( + NEW.id, + NEW.reason, + COALESCE(NEW.is_equivalence, FALSE), + NEW.dualized_from + ); + + INSERT INTO functor_implication_assumptions (implication_id, property_id) + SELECT NEW.id, value + FROM json_each(NEW.assumptions); + + INSERT INTO functor_implication_source_assumptions (implication_id, property_id) + SELECT NEW.id, value + FROM json_each(NEW.source_assumptions); + + INSERT INTO functor_implication_target_assumptions (implication_id, property_id) + SELECT NEW.id, value + FROM json_each(NEW.target_assumptions); + + INSERT INTO functor_implication_conclusions (implication_id, property_id) + SELECT NEW.id, value + FROM json_each(NEW.conclusions); +END; \ No newline at end of file From 5371ef7c4eef38fcfd0d33115715d8709b69f942 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 21 Mar 2026 10:32:28 +0100 Subject: [PATCH 02/10] add properties of functors and their implications --- .vscode/settings.json | 4 + database/data/004_prefixes.sql | 3 +- database/data/020_functor-properties.sql | 169 +++++++++++++++++++++ database/data/021_functor-implications.sql | 105 +++++++++++++ 4 files changed, 280 insertions(+), 1 deletion(-) create mode 100644 database/data/020_functor-properties.sql create mode 100644 database/data/021_functor-implications.sql diff --git a/.vscode/settings.json b/.vscode/settings.json index d4dc5d2..d39d954 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -43,11 +43,14 @@ "coequalizer", "coequalizers", "cofiltered", + "cofinitary", "cogenerates", "cogenerator", "cokernel", "colimit", "colimits", + "comonad", + "comonadic", "conormal", "coprime", "coproduct", @@ -121,6 +124,7 @@ "rng", "rngs", "Rosicky", + "saft", "Schapira", "semisimple", "setoid", diff --git a/database/data/004_prefixes.sql b/database/data/004_prefixes.sql index 26e088f..93aff50 100644 --- a/database/data/004_prefixes.sql +++ b/database/data/004_prefixes.sql @@ -4,4 +4,5 @@ INSERT INTO prefixes (prefix, negation) VALUES ('is an', 'is not an'), ('has', 'does not have'), ('has a', 'does not have a'), - ('has an', 'does not have an'); \ No newline at end of file + ('has an', 'does not have an'), + ('', 'does not'); \ No newline at end of file diff --git a/database/data/020_functor-properties.sql b/database/data/020_functor-properties.sql new file mode 100644 index 0000000..3357c72 --- /dev/null +++ b/database/data/020_functor-properties.sql @@ -0,0 +1,169 @@ +INSERT INTO functor_properties ( + id, + prefix, + description, + nlab_link, + invariant_under_equivalences, + dual_property_id +) +VALUES + ( + 'faithful', + 'is', + 'A functor is faithful when it is injective on Hom-sets: If $F(f)=F(g)$, then $f=g$.', + 'https://ncatlab.org/nlab/show/faithful+functor', + TRUE, + 'faithful' + ), + ( + 'full', + 'is', + 'A functor is full when it is surjective on Hom-sets: Every morphism $F(A) \to F(B)$ is induced by a morphism $A \to B$.', + 'https://ncatlab.org/nlab/show/full+functor', + TRUE, + 'full' + ), + ( + 'essentially surjective', + 'is', + 'A functor $F : \mathcal{C} \to \mathcal{D}$ is essentially surjective when every object $Y \in \mathcal{D}$ is isomorphic to $F(X)$ for some $X \in \mathcal{C}$.', + 'https://ncatlab.org/nlab/show/essentially+surjective+functor', + TRUE, + 'essentially surjective' + ), + ( + 'equivalence', + 'is an', + 'A functor is an equivalence if it has a pseudo-inverse functor.', + 'https://ncatlab.org/nlab/show/equivalence+of+categories', + TRUE, + 'equivalence' + ), + ( + 'continuous', + 'is', + 'A functor is continuous when it preserves all small limits.', + 'https://ncatlab.org/nlab/show/continuous+functor', + TRUE, + 'cocontinuous' + ), + ( + 'cocontinuous', + 'is', + 'A functor is cocontinuous when it preserves all small colimits.', + 'https://ncatlab.org/nlab/show/cocontinuous+functor', + TRUE, + 'continuous' + ), + ( + 'preserves products', + '', + 'A functor $F$ preserves products when for every family of objects $(A_i)$ in the source whose product $\prod_i A_i$ exists, also the product $\prod_i F(A_i)$ exists in the target and such that the canonical morphism $F(\prod_i A_i) \to \prod_i F(A_i)$ is an isomorphism.', + NULL, + TRUE, + 'preserves coproducts' + ), + ( + 'preserves coproducts', + '', + 'A functor $F$ preserves coproducts when for every family of objects $(A_i)$ in the source whose coproduct $\prod_i A_i$ exists, also the coproduct $\coprod_i F(A_i)$ exists in the target and such that the canonical morphism $\coprod_i F(A_i) \to F(\coprod_i A_i)$ is an isomorphism.', + NULL, + TRUE, + 'preserves products' + ), + ( + 'preserves equalizers', + '', + 'A functor $F$ preserves equalizers when for every parallel pair of morphisms $f,g : A \to B$ whose equalizer $i : E \to A$ exists, also $F(i) : F(E) \to F(A)$ is an equalizer of $F(f),F(g) : F(A) \to F(B)$.', + NULL, + TRUE, + 'preserves coequalizers' + ), + ( + 'preserves coequalizers', + '', + 'A functor $F$ preserves coequalizers when for every parallel pair of morphisms $f,g : A \to B$ whose coequalizer $p : B \to Q$ exists, also $F(p) : F(B) \to F(Q)$ is an coequalizer of $F(f),F(g) : F(A) \to F(B)$.', + NULL, + TRUE, + 'preserves equalizers' + ), + ( + 'left adjoint', + 'is a', + 'A functor $F : \mathcal{C} \to \mathcal{D}$ is a left adjoint when there is a functor $G : \mathcal{D} \to \mathcal{C}$ such that there are natural bijections $\hom(F(A),B) \cong \hom(A,G(B))$.', + 'https://ncatlab.org/nlab/show/left+adjoint', + TRUE, + 'right adjoint' + ), + ( + 'right adjoint', + 'is a', + 'A functor $F : \mathcal{C} \to \mathcal{D}$ is a right adjoint when there is a functor $G : \mathcal{D} \to \mathcal{C}$ such that there are natural bijections $\hom(G(A),B) \cong \hom(A,F(B))$.', + 'https://ncatlab.org/nlab/show/right+adjoint', + TRUE, + 'left adjoint' + ), + ( + 'monadic', + 'is', + 'A functor $F : \mathcal{C} \to \mathcal{D}$ is monadic when there is a monad $T$ on $\mathcal{D}$ such that $F$ is equivalent to the forgetful functor $U^T : \mathbf{Alg}(T) \to \mathcal{D}$.', + 'https://ncatlab.org/nlab/show/monadic+functor', + TRUE, + 'comonadic' + ), + ( + 'comonadic', + 'is', + 'A functor $F : \mathcal{C} \to \mathcal{D}$ is comonadic when there is a comonad $T$ on $\mathcal{D}$ such that $F$ is equivalent to the forgetful functor $U^T : \mathbf{CoAlg}(T) \to \mathcal{D}$.', + 'https://ncatlab.org/nlab/show/comonadic+functor', + TRUE, + 'monadic' + ), + ( + 'conservative', + 'is', + 'A functor $F : \mathcal{C} \to \mathcal{D}$ is conservative when it is isomorphic-reflecting: If $f$ is a morphism in $\mathcal{C}$ such that $F(f)$ is an isomorphism, then $f$ is an isomorphism.', + 'https://ncatlab.org/nlab/show/conservative+functor', + TRUE, + 'conservative' + ), + ( + 'finitary', + 'is', + 'A functor is finitary when it preserves filtered colimits.', + 'https://ncatlab.org/nlab/show/finitary+functor', + TRUE, + 'cofinitary' + ), + ( + 'cofinitary', + 'is', + 'A functor is cofinitary when it preserves filtered limits.', + NULL, + TRUE, + 'finitary' + ), + ( + 'left exact', + 'is', + 'A functor is left exact when it preserves finite limits.', + 'https://ncatlab.org/nlab/show/exact+functor', + TRUE, + 'right exact' + ), + ( + 'right exact', + 'is', + 'A functor is right exact when it preserves finite colimits.', + 'https://ncatlab.org/nlab/show/exact+functor', + TRUE, + 'left exact' + ), + ( + 'exact', + 'is', + 'A functor is exact when it is left exact and right exact.', + 'https://ncatlab.org/nlab/show/exact+functor', + TRUE, + 'exact' + ); diff --git a/database/data/021_functor-implications.sql b/database/data/021_functor-implications.sql new file mode 100644 index 0000000..792c4b1 --- /dev/null +++ b/database/data/021_functor-implications.sql @@ -0,0 +1,105 @@ +INSERT INTO functor_implication_input ( + id, + assumptions, + source_assumptions, + target_assumptions, + conclusions, + reason, + is_equivalence +) +VALUES + ( + 'equivalence_criterion', + '["full", "faithful", "essentially surjective"]', + '[]', + '[]', + '["equivalence"]', + 'TBA.', -- FIXME + TRUE + ), + ( + 'continuous_consequences', -- TODO: dualize automatically + '["continuous"]', + '[]', + '[]', + '["preserves products", "preserves equalizers", "cofinitary"]', + 'This is trivial.', + FALSE + ), + ( + 'dual_continuous_consequences', -- TODO: remove this later + '["cocontinuous"]', + '[]', + '[]', + '["preserves coproducts", "preserves coequalizers", "finitary"]', + 'This is trivial.', + FALSE + ), + ( + 'continuous_criterion', + '["preserves products", "preserves equalizers"]', + '["products"]', + '[]', + '["continuous"]', + 'TBA.', -- FIXME + FALSE + ), + ( + 'continuous_criterion_filtered', + '["left exact", "cofinitary"]', + '["finitely complete"]', + '[]', + '["continuous"]', + 'This is because every limit can be written as a filtered limit of finite limits.', + FALSE + ), + ( + 'exact_definition', + '["exact"]', + '[]', + '[]', + '["left exact", "right exact"]', + 'This holds by definition.', + TRUE + ), + ( + 'equivalence_consequences', -- TODO: dualize automatically + '["equivalence"]', + '[]', + '[]', + '["continuous", "right adjoint"]', + 'Easy.', + FALSE + ), + ( + 'right_adjoint_consequences', -- TODO: dualize automatically + '["right adjoint"]', + '[]', + '[]', + '["continuous"]', + 'TBA.', -- FIXME + FALSE + ), + ( + 'saft', -- TODO: dualize automatically, + '["continuous"]', + '["complete", "locally small", "well-powered", "cogenerator"]', + '["locally small"]', + '["right adjoint"]', + 'This is the Special Adjoint Functor Theorem. The proof can be found, for example, at the nLab.', + FALSE + ), + ( + 'monadic_consequences', -- TODO: dualize automatically + '["monadic"]', + '[]', + '[]', + '["faithful", "right adjoint", "conservative"]', + 'This is clear since the forgetful functor from the category of $T$-algebras has these properties, where $T$ is any monad.', + FALSE + ); + + -- TODO: remove this later: + UPDATE functor_implications + SET dualized_from = 'continuous_consequences' + WHERE id = 'dual_continuous_consequences'; \ No newline at end of file From ee4c3a0687f215febde40ba12c578b50fdced890 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 21 Mar 2026 10:33:39 +0100 Subject: [PATCH 03/10] make property lists more generic --- src/components/PropertyList.svelte | 5 +++-- src/lib/commons/property.url.ts | 5 +++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/components/PropertyList.svelte b/src/components/PropertyList.svelte index 70eb4a3..b6326b7 100644 --- a/src/components/PropertyList.svelte +++ b/src/components/PropertyList.svelte @@ -9,9 +9,10 @@ reason?: string | null }[] description?: string + type?: 'category' | 'functor' } - let { properties, description }: Props = $props() + let { properties, description, type = 'category' }: Props = $props() {#if description} @@ -24,7 +25,7 @@
  • {prefix} - {id} + {id}
    • {/each} diff --git a/src/lib/commons/property.url.ts b/src/lib/commons/property.url.ts index e94273a..02e5afb 100644 --- a/src/lib/commons/property.url.ts +++ b/src/lib/commons/property.url.ts @@ -24,6 +24,7 @@ export function decode_property_ID(str: string): string { return decoded } -export function get_property_url(id: string) { - return `/property/${encode_property_ID(id)}` +export function get_property_url(id: string, type: 'category' | 'functor' = 'category') { + if (type === 'category') return `/property/${encode_property_ID(id)}` + return `/functor-property/${encode_property_ID(id)}` } From 6ffef2aec77a6caf75b638ff4e954ed5cbc6ebb2 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 21 Mar 2026 10:36:33 +0100 Subject: [PATCH 04/10] display functor properties and implications in app --- src/components/Nav.svelte | 12 +++ src/components/NavMobile.svelte | 14 +++ src/lib/commons/types.ts | 37 ++++++++ src/lib/server/utils.ts | 30 +++++++ .../functor-implication/[id]/+page.server.ts | 34 ++++++++ .../functor-implication/[id]/+page.svelte | 85 +++++++++++++++++++ .../functor-implications/+page.server.ts | 31 +++++++ src/routes/functor-implications/+page.svelte | 24 ++++++ src/routes/functor-properties/+page.server.ts | 16 ++++ src/routes/functor-properties/+page.svelte | 15 ++++ .../functor-property/[id]/+page.server.ts | 32 +++++++ src/routes/functor-property/[id]/+page.svelte | 46 ++++++++++ 12 files changed, 376 insertions(+) create mode 100644 src/routes/functor-implication/[id]/+page.server.ts create mode 100644 src/routes/functor-implication/[id]/+page.svelte create mode 100644 src/routes/functor-implications/+page.server.ts create mode 100644 src/routes/functor-implications/+page.svelte create mode 100644 src/routes/functor-properties/+page.server.ts create mode 100644 src/routes/functor-properties/+page.svelte create mode 100644 src/routes/functor-property/[id]/+page.server.ts create mode 100644 src/routes/functor-property/[id]/+page.svelte diff --git a/src/components/Nav.svelte b/src/components/Nav.svelte index de87888..44cdede 100644 --- a/src/components/Nav.svelte +++ b/src/components/Nav.svelte @@ -30,6 +30,18 @@ { href: '/implications', text: 'Implications', icon: faArrowsSplitUpAndLeft }, { href: '/compare', text: 'Compare', icon: faChartBar, nested: '/compare' }, { href: '/search', text: 'Search', icon: faSearch }, + { + href: '/functor-properties', + text: 'Functor properties', + nested: '/functor-property', + icon: faList, + }, + { + href: '/functor-implications', + text: 'Functor implications', + nested: '/functor-implication', + icon: faArrowsSplitUpAndLeft, + }, ] diff --git a/src/components/NavMobile.svelte b/src/components/NavMobile.svelte index 4510341..976f2aa 100644 --- a/src/components/NavMobile.svelte +++ b/src/components/NavMobile.svelte @@ -62,6 +62,20 @@ + +
  • + + Functor properties + + +
    • + +
  • + + Functor implications + + +
      • diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index fff90eb..bda4db8 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -82,3 +82,40 @@ export type SpecialMorphism = { description: string reason: string } +export type FunctorPropertyDB = { + id: string + prefix: string + description: string + nlab_link: string | null + invariant_under_equivalences: number + dual_property_id: string | null +} + +export type FunctorProperty = Replace< + FunctorPropertyDB, + { + invariant_under_equivalences: boolean + } +> + +export type FunctorImplicationDB = { + id: string + is_equivalence: number + reason: string + assumptions: string + conclusions: string + source_assumptions: string + target_assumptions: string + dualized_from?: string | null +} + +export type FunctorImplicationDisplay = Replace< + FunctorImplicationDB, + { + is_equivalence: boolean + assumptions: string[] + conclusions: string[] + source_assumptions: string[] + target_assumptions: string[] + } +> diff --git a/src/lib/server/utils.ts b/src/lib/server/utils.ts index 0514cd3..11ea436 100644 --- a/src/lib/server/utils.ts +++ b/src/lib/server/utils.ts @@ -1,4 +1,8 @@ import type { + FunctorImplicationDB, + FunctorImplicationDisplay, + FunctorProperty, + FunctorPropertyDB, ImplicationDB, ImplicationDisplay, PropertyDB, @@ -40,6 +44,32 @@ export function to_placeholders(arr: string[]): string { return arr.map(() => '?').join(', ') } +export function display_functor_property(property: FunctorPropertyDB): FunctorProperty { + return { + id: property.id, + prefix: property.prefix, + description: property.description, + dual_property_id: property.dual_property_id, + nlab_link: property.nlab_link, + invariant_under_equivalences: Boolean(property.invariant_under_equivalences), + } +} + +export function display_functor_implication( + implication: FunctorImplicationDB, +): FunctorImplicationDisplay { + return { + id: implication.id, + is_equivalence: Boolean(implication.is_equivalence), + reason: implication.reason, + assumptions: JSON.parse(implication.assumptions), + source_assumptions: JSON.parse(implication.source_assumptions), + target_assumptions: JSON.parse(implication.target_assumptions), + conclusions: JSON.parse(implication.conclusions), + dualized_from: implication.dualized_from, + } +} + const crawler_detector = new Crawler() function is_bot(request: Request): boolean { diff --git a/src/routes/functor-implication/[id]/+page.server.ts b/src/routes/functor-implication/[id]/+page.server.ts new file mode 100644 index 0000000..102eba6 --- /dev/null +++ b/src/routes/functor-implication/[id]/+page.server.ts @@ -0,0 +1,34 @@ +import { render_nested_formulas } from '$lib/server/rendering' +import { query } from '$lib/server/db' +import sql from 'sql-template-tag' +import { error } from '@sveltejs/kit' +import type { FunctorImplicationDB, FunctorImplicationDisplay } from '$lib/commons/types' +import { display_functor_implication } from '$lib/server/utils' + +export const prerender = true + +export const load = async (event) => { + const id = event.params.id + + const { rows, err } = await query(sql` + SELECT + id, + is_equivalence, + reason, + assumptions, + conclusions, + source_assumptions, + target_assumptions, + dualized_from + FROM functor_implications_view + WHERE id = ${id} + `) + + if (err) error(500, 'Could not load implication') + + if (!rows.length) error(404, `Could not find implication with ID '${id}'`) + + const implication: FunctorImplicationDisplay = display_functor_implication(rows[0]) + + return render_nested_formulas({ implication }) +} diff --git a/src/routes/functor-implication/[id]/+page.svelte b/src/routes/functor-implication/[id]/+page.svelte new file mode 100644 index 0000000..147aa72 --- /dev/null +++ b/src/routes/functor-implication/[id]/+page.svelte @@ -0,0 +1,85 @@ + + + + +

      Implication Details

      + +

      + Assumptions: + + {#each data.implication.assumptions as property, index} + {property}{#if index < data.implication.assumptions.length - 1} + ,  + {/if} + {/each} +

      + +{#if data.implication.source_assumptions.length} +

      + Assumptions on source category: + + {#each data.implication.source_assumptions as property, index} + {property}{#if index < data.implication.source_assumptions.length - 1} + ,  + {/if} + {/each} +

      +{/if} + +{#if data.implication.target_assumptions.length} +

      + Assumptions on target category: + + {#each data.implication.target_assumptions as property, index} + {property}{#if index < data.implication.target_assumptions.length - 1} + ,  + {/if} + {/each} +

      +{/if} + +

      + Conclusions: + {#each data.implication.conclusions as property, index} + {property}{#if index < data.implication.conclusions.length - 1} + ,  + {/if} + {/each} +

      + +{#if data.implication.is_equivalence} +

      + + This is an equivalence. +

      +{/if} + +{#if data.implication.dualized_from} +

      + This implication has been dualized from + this implication + . +

      +{:else} +

      + Reason: + {@html data.implication.reason} +

      +{/if} + + + +
      {JSON.stringify(data.implication, null, 4)}
      diff --git a/src/routes/functor-implications/+page.server.ts b/src/routes/functor-implications/+page.server.ts new file mode 100644 index 0000000..8fc1e87 --- /dev/null +++ b/src/routes/functor-implications/+page.server.ts @@ -0,0 +1,31 @@ +import { render_nested_formulas } from '$lib/server/rendering' +import { query } from '$lib/server/db' +import sql from 'sql-template-tag' +import { error } from '@sveltejs/kit' +import type { FunctorImplicationDB, FunctorImplicationDisplay } from '$lib/commons/types' +import { display_functor_implication } from '$lib/server/utils' + +export const prerender = true + +export const load = async () => { + const { rows, err } = await query(sql` + SELECT + id, + is_equivalence, + reason, + assumptions, + conclusions, + source_assumptions, + target_assumptions + FROM functor_implications_view + ORDER BY lower(assumptions) || ' ' || lower(conclusions) + `) + + if (err) error(500, 'Could not load implications') + + const implications: FunctorImplicationDisplay[] = rows.map( + display_functor_implication, + ) + + return render_nested_formulas({ implications }) +} diff --git a/src/routes/functor-implications/+page.svelte b/src/routes/functor-implications/+page.svelte new file mode 100644 index 0000000..e07477e --- /dev/null +++ b/src/routes/functor-implications/+page.svelte @@ -0,0 +1,24 @@ + + + + +

      List of implications of functors

      + + + +
        + {#each data.implications as implication (implication.id)} +
      • + {implication.id} +
        • + {/each} +
      diff --git a/src/routes/functor-properties/+page.server.ts b/src/routes/functor-properties/+page.server.ts new file mode 100644 index 0000000..5bad5ec --- /dev/null +++ b/src/routes/functor-properties/+page.server.ts @@ -0,0 +1,16 @@ +import type { PropertyShort } from '$lib/commons/types' +import { query } from '$lib/server/db' +import { error } from '@sveltejs/kit' +import sql from 'sql-template-tag' + +export const load = async () => { + const { rows: properties, err } = await query(sql` + SELECT id, prefix + FROM functor_properties + ORDER BY lower(id) + `) + + if (err) error(500, 'Could not load properties') + + return { properties } +} diff --git a/src/routes/functor-properties/+page.svelte b/src/routes/functor-properties/+page.svelte new file mode 100644 index 0000000..b34c847 --- /dev/null +++ b/src/routes/functor-properties/+page.svelte @@ -0,0 +1,15 @@ + + + + +

      Properties of Functors

      + + diff --git a/src/routes/functor-property/[id]/+page.server.ts b/src/routes/functor-property/[id]/+page.server.ts new file mode 100644 index 0000000..b493cb6 --- /dev/null +++ b/src/routes/functor-property/[id]/+page.server.ts @@ -0,0 +1,32 @@ +import { decode_property_ID } from '$lib/commons/property.url.js' +import type { FunctorPropertyDB } from '$lib/commons/types' +import { query } from '$lib/server/db' +import { render_nested_formulas } from '$lib/server/rendering.js' +import { display_functor_property } from '$lib/server/utils' +import { error } from '@sveltejs/kit' +import sql from 'sql-template-tag' + +export const load = async (event) => { + const id = decode_property_ID(event.params.id) + + const { rows: properties, err } = await query(sql` + SELECT + id, + prefix, + description, + nlab_link, + invariant_under_equivalences, + dual_property_id + FROM + functor_properties + WHERE id = ${id} + `) + + if (err) error(500, 'Could not load properties') + + if (!properties.length) error(404, `There is no property with ID '${id}'`) + + const property = display_functor_property(properties[0]) + + return render_nested_formulas({ property }) +} diff --git a/src/routes/functor-property/[id]/+page.svelte b/src/routes/functor-property/[id]/+page.svelte new file mode 100644 index 0000000..f716408 --- /dev/null +++ b/src/routes/functor-property/[id]/+page.svelte @@ -0,0 +1,46 @@ + + + + +

      {property.id}

      + +

      + {@html property.description} + + {#if property.invariant_under_equivalences === false} + Warning: This property is not invariant under equivalences. + {/if} +

      + +{#if property.dual_property_id || property.nlab_link} +
        + {#if property.dual_property_id} +
      • + Dual property: + {property.dual_property_id} + {#if property.dual_property_id === property.id} + (self-dual) + {/if} +
        • + {/if} + + {#if property.nlab_link} +
      • + nLab Link +
        • + {/if} +
      +{/if} + +

      + +

      From 3d0e144fd7a128bf95a152ff348f116bd5c4cb0d Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 21 Mar 2026 11:08:19 +0100 Subject: [PATCH 05/10] add mode selector --- src/components/Heading.svelte | 15 +++++ src/components/ModeSelector.svelte | 22 ++++++ src/components/Nav.svelte | 41 +++++++++-- src/components/NavMobile.svelte | 105 ++++++++++++++++------------- src/lib/states/app.mode.svelte.ts | 5 ++ src/routes/app.css | 6 +- 6 files changed, 141 insertions(+), 53 deletions(-) create mode 100644 src/components/ModeSelector.svelte create mode 100644 src/lib/states/app.mode.svelte.ts diff --git a/src/components/Heading.svelte b/src/components/Heading.svelte index 1873c48..89d73e5 100644 --- a/src/components/Heading.svelte +++ b/src/components/Heading.svelte @@ -1,6 +1,7 @@ + + + + + + diff --git a/src/components/Nav.svelte b/src/components/Nav.svelte index 44cdede..ee85c43 100644 --- a/src/components/Nav.svelte +++ b/src/components/Nav.svelte @@ -1,5 +1,6 @@