(
+ // specific information for the morphism
+ sql`
+ SELECT
+ c.id AS category,
+ c.name AS category_name,
+ c.notation AS category_notation
+ FROM morphisms m
+ INNER JOIN structures AS c ON c.id = m.category
+ WHERE m.id = ${id}
+ `,
+ )
+
+ if (err) error(500, 'Could not load morphism')
+
+ if (!morphisms.length) error(404, `Could not find morphism with ID '${id}'`)
+
+ return morphisms[0]
+}
diff --git a/src/pages/ImplicationPage.svelte b/src/pages/ImplicationPage.svelte
index 39db6aa7..3dc99f43 100644
--- a/src/pages/ImplicationPage.svelte
+++ b/src/pages/ImplicationPage.svelte
@@ -42,7 +42,7 @@
{#each Object.entries(implication.mapped_assumptions) as [map, list]}
{#if list?.length}
- Assumptions on {map} {mapped_types[map]}:
+ Requirements of the {map}:
{#each list as property, index}
{property}
{/if}
+ {#if type === 'morphism'}
+
+
+
+ The morphism application is still in its early stages. More morphisms will be added
+ soon.
+
+ {/if}
+
diff --git a/src/routes/missing/+page.server.ts b/src/routes/missing/+page.server.ts
index 7017258e..b25f2c69 100644
--- a/src/routes/missing/+page.server.ts
+++ b/src/routes/missing/+page.server.ts
@@ -1,29 +1,29 @@
import { fetch_missing_data } from '$lib/server/fetchers/missing_data'
import { fetch_categories_with_missing_morphisms } from '$lib/server/fetchers/category'
+import { STRUCTURES } from '$lib/commons/structures'
export const load = () => {
const categories_with_missing_morphisms = fetch_categories_with_missing_morphisms()
- const missing_category_data = fetch_missing_data('category')
- const missing_functor_data = fetch_missing_data('functor')
+ const missing_data = Object.fromEntries(
+ STRUCTURES.map((type) => [type, fetch_missing_data(type)]),
+ )
+
+ function select(
+ selector: (data: (typeof missing_data)[keyof typeof missing_data]) => T,
+ ) {
+ return Object.fromEntries(
+ STRUCTURES.map((type) => [type, selector(missing_data[type])]),
+ )
+ }
return {
- structures_with_unknown_properties: {
- category: missing_category_data.structures_with_unknown_properties,
- functor: missing_functor_data.structures_with_unknown_properties,
- },
- unknown_totals: {
- category: missing_category_data.total_unknown_property_pairs,
- functor: missing_functor_data.total_unknown_property_pairs,
- },
- undistinguishable_pairs: {
- category: missing_category_data.undistinguishable_structure_pairs,
- functor: missing_functor_data.undistinguishable_structure_pairs,
- },
- missing_combinations: {
- category: missing_category_data.missing_combinations,
- functor: missing_functor_data.missing_combinations,
- },
+ structures_with_unknown_properties: select(
+ (data) => data.structures_with_unknown_properties,
+ ),
+ unknown_totals: select((data) => data.total_unknown_property_pairs),
+ undistinguishable_pairs: select((data) => data.undistinguishable_structure_pairs),
+ missing_combinations: select((data) => data.missing_combinations),
categories_with_missing_morphisms,
}
}
diff --git a/src/routes/missing/+page.svelte b/src/routes/missing/+page.svelte
index 117a5191..b566f809 100644
--- a/src/routes/missing/+page.svelte
+++ b/src/routes/missing/+page.svelte
@@ -87,33 +87,35 @@
{#each STRUCTURES as type}
{@const combinations = data.missing_combinations[type]}
-
- Missing {type} combinations
+ {#if combinations.length > 0}
+
+ Missing {type} combinations
-
- Among the consistent {type} combinations of the form p ∧ ¬q, the following
- are not yet witnessed by a {type} in the database or its dual. If some of these
- combinations are
- inconsistent, this indicates that some
- implication is missing.
-
+
+ Among the consistent {type} combinations of the form p ∧ ¬q, the following
+ are not yet witnessed by a {type} in the database or its dual. If some of these
+ combinations are
+ inconsistent, this indicates that some
+ implication is missing.
+
-
-
- Show all {combinations.length} combinations
-
-
-
- {#each combinations as [p, q]}
- -
- {p} ∧ ¬{q}
-
- {/each}
-
-
-
+
+
+ Show all {combinations.length} combinations
+
+
+
+ {#each combinations as [p, q]}
+ -
+ {p} ∧ ¬{q}
+
+ {/each}
+
+
+
+ {/if}
{/each}
diff --git a/src/routes/morphism-comparison/+page.server.ts b/src/routes/morphism-comparison/+page.server.ts
new file mode 100644
index 00000000..27b026bc
--- /dev/null
+++ b/src/routes/morphism-comparison/+page.server.ts
@@ -0,0 +1,5 @@
+import { fetch_structures } from '$lib/server/fetchers/structures'
+
+export const load = () => {
+ return fetch_structures('morphism')
+}
diff --git a/src/routes/morphism-comparison/+page.svelte b/src/routes/morphism-comparison/+page.svelte
new file mode 100644
index 00000000..626b192e
--- /dev/null
+++ b/src/routes/morphism-comparison/+page.svelte
@@ -0,0 +1,7 @@
+
+
+
diff --git a/src/routes/morphism-comparison/[...ids]/+page.server.ts b/src/routes/morphism-comparison/[...ids]/+page.server.ts
new file mode 100644
index 00000000..12443fd9
--- /dev/null
+++ b/src/routes/morphism-comparison/[...ids]/+page.server.ts
@@ -0,0 +1,12 @@
+import { fetch_comparison_result } from '$lib/server/fetchers/comparison'
+import { cache_page } from '$lib/server/utils'
+
+export const prerender = false
+
+export const load = (event) => {
+ const compared_ids = event.params.ids.split('/')
+
+ return fetch_comparison_result(compared_ids, 'morphism', () => {
+ cache_page(event)
+ })
+}
diff --git a/src/routes/morphism-comparison/[...ids]/+page.svelte b/src/routes/morphism-comparison/[...ids]/+page.svelte
new file mode 100644
index 00000000..11f4d1e6
--- /dev/null
+++ b/src/routes/morphism-comparison/[...ids]/+page.svelte
@@ -0,0 +1,7 @@
+
+
+
diff --git a/src/routes/morphism-implication/[id]/+page.server.ts b/src/routes/morphism-implication/[id]/+page.server.ts
new file mode 100644
index 00000000..bb302106
--- /dev/null
+++ b/src/routes/morphism-implication/[id]/+page.server.ts
@@ -0,0 +1,8 @@
+import { fetch_implication } from '$lib/server/fetchers/implication'
+import { render_nested_formulas } from '$lib/server/formulas'
+
+export const load = (event) => {
+ const id = event.params.id
+
+ return render_nested_formulas(fetch_implication('morphism', id))
+}
diff --git a/src/routes/morphism-implication/[id]/+page.svelte b/src/routes/morphism-implication/[id]/+page.svelte
new file mode 100644
index 00000000..a97e46ff
--- /dev/null
+++ b/src/routes/morphism-implication/[id]/+page.svelte
@@ -0,0 +1,7 @@
+
+
+
diff --git a/src/routes/morphism-implications/+page.server.ts b/src/routes/morphism-implications/+page.server.ts
new file mode 100644
index 00000000..c3c4e42b
--- /dev/null
+++ b/src/routes/morphism-implications/+page.server.ts
@@ -0,0 +1,8 @@
+import { render_nested_formulas } from '$lib/server/formulas'
+import { fetch_implications } from '$lib/server/fetchers/implications'
+
+export const load = () => {
+ const { implications } = fetch_implications('morphism')
+
+ return render_nested_formulas({ implications })
+}
diff --git a/src/routes/morphism-implications/+page.svelte b/src/routes/morphism-implications/+page.svelte
new file mode 100644
index 00000000..fd3605ac
--- /dev/null
+++ b/src/routes/morphism-implications/+page.svelte
@@ -0,0 +1,15 @@
+
+
+
+ {#snippet hints()}
+
+ *Deductions from these implications are automatically incorporated into each
+ morphism whenever applicable. Moreover, implications are automatically
+ dualized when the corresponding dual properties exist.
+
+ {/snippet}
+
diff --git a/src/routes/morphism-properties/+page.server.ts b/src/routes/morphism-properties/+page.server.ts
new file mode 100644
index 00000000..65095e1b
--- /dev/null
+++ b/src/routes/morphism-properties/+page.server.ts
@@ -0,0 +1,5 @@
+import { fetch_grouped_properties_and_tags } from '$lib/server/fetchers/properties'
+
+export const load = () => {
+ return fetch_grouped_properties_and_tags('morphism')
+}
diff --git a/src/routes/morphism-properties/+page.svelte b/src/routes/morphism-properties/+page.svelte
new file mode 100644
index 00000000..dadefb7f
--- /dev/null
+++ b/src/routes/morphism-properties/+page.svelte
@@ -0,0 +1,7 @@
+
+
+
diff --git a/src/routes/morphism-properties/[tag]/+page.server.ts b/src/routes/morphism-properties/[tag]/+page.server.ts
new file mode 100644
index 00000000..ccbb6896
--- /dev/null
+++ b/src/routes/morphism-properties/[tag]/+page.server.ts
@@ -0,0 +1,11 @@
+import { fetch_tagged_properties } from '$lib/server/fetchers/properties'
+import { fetch_property_tags } from '$lib/server/fetchers/tags'
+import type { EntryGenerator } from './$types'
+
+export const entries: EntryGenerator = () => {
+ return fetch_property_tags('morphism')
+}
+
+export const load = (event) => {
+ return fetch_tagged_properties('morphism', event.params.tag)
+}
diff --git a/src/routes/morphism-properties/[tag]/+page.svelte b/src/routes/morphism-properties/[tag]/+page.svelte
new file mode 100644
index 00000000..62fb6cb9
--- /dev/null
+++ b/src/routes/morphism-properties/[tag]/+page.svelte
@@ -0,0 +1,7 @@
+
+
+
diff --git a/src/routes/morphism-property/[id]/+page.server.ts b/src/routes/morphism-property/[id]/+page.server.ts
new file mode 100644
index 00000000..3ce350d5
--- /dev/null
+++ b/src/routes/morphism-property/[id]/+page.server.ts
@@ -0,0 +1,11 @@
+import { render_nested_formulas } from '$lib/server/formulas'
+import { decode_property_ID } from '$lib/commons/property.url'
+import { fetch_property } from '$lib/server/fetchers/property'
+
+export const load = (event) => {
+ const id = decode_property_ID(event.params.id)
+
+ const property_data = fetch_property('morphism', id)
+
+ return render_nested_formulas(property_data)
+}
diff --git a/src/routes/morphism-property/[id]/+page.svelte b/src/routes/morphism-property/[id]/+page.svelte
new file mode 100644
index 00000000..acb5718b
--- /dev/null
+++ b/src/routes/morphism-property/[id]/+page.svelte
@@ -0,0 +1,7 @@
+
+
+
diff --git a/src/routes/morphism-search/+page.server.ts b/src/routes/morphism-search/+page.server.ts
new file mode 100644
index 00000000..6ba761c3
--- /dev/null
+++ b/src/routes/morphism-search/+page.server.ts
@@ -0,0 +1,5 @@
+import { get_property_ids } from '$lib/server/fetchers/properties'
+
+export const load = () => {
+ return { all_properties: get_property_ids('morphism') }
+}
diff --git a/src/routes/morphism-search/+page.svelte b/src/routes/morphism-search/+page.svelte
new file mode 100644
index 00000000..d62dc5d3
--- /dev/null
+++ b/src/routes/morphism-search/+page.svelte
@@ -0,0 +1,13 @@
+
+
+
+ Search for morphism with certain properties while excluding others. For example, you
+ can look for morphisms which are monomorphisms and epimorphisms,
+ but no isomorphisms.
+
diff --git a/src/routes/morphism-search/results/+page.server.ts b/src/routes/morphism-search/results/+page.server.ts
new file mode 100644
index 00000000..390cfa6b
--- /dev/null
+++ b/src/routes/morphism-search/results/+page.server.ts
@@ -0,0 +1,13 @@
+import { fetch_search_results } from '$lib/server/fetchers/search'
+import { cache_page } from '$lib/server/utils'
+
+export const prerender = false
+
+export const load = (event) => {
+ const satisfied_query = event.url.searchParams.get('satisfied')
+ const unsatisfied_query = event.url.searchParams.get('unsatisfied')
+
+ return fetch_search_results(satisfied_query, unsatisfied_query, 'morphism', () =>
+ cache_page(event),
+ )
+}
diff --git a/src/routes/morphism-search/results/+page.svelte b/src/routes/morphism-search/results/+page.svelte
new file mode 100644
index 00000000..2a2557f4
--- /dev/null
+++ b/src/routes/morphism-search/results/+page.svelte
@@ -0,0 +1,7 @@
+
+
+
diff --git a/src/routes/morphism/[id]/+page.server.ts b/src/routes/morphism/[id]/+page.server.ts
new file mode 100644
index 00000000..6923eaf4
--- /dev/null
+++ b/src/routes/morphism/[id]/+page.server.ts
@@ -0,0 +1,34 @@
+import { fetch_morphism } from '$lib/server/fetchers/morphism'
+import { fetch_structure } from '$lib/server/fetchers/structure'
+import { render_nested_formulas } from '$lib/server/formulas'
+
+export const load = (event) => {
+ const id = event.params.id
+
+ const {
+ structure,
+ related_structures,
+ tags,
+ satisfied_properties,
+ unsatisfied_properties,
+ unknown_properties,
+ undecidable_properties,
+ undistinguishable_structures,
+ comments,
+ } = fetch_structure('morphism', id)
+
+ const morphism = fetch_morphism(id)
+
+ return render_nested_formulas({
+ structure,
+ morphism,
+ related_structures,
+ tags,
+ satisfied_properties,
+ unsatisfied_properties,
+ unknown_properties,
+ undecidable_properties,
+ undistinguishable_structures,
+ comments,
+ })
+}
diff --git a/src/routes/morphism/[id]/+page.svelte b/src/routes/morphism/[id]/+page.svelte
new file mode 100644
index 00000000..0e2550a6
--- /dev/null
+++ b/src/routes/morphism/[id]/+page.svelte
@@ -0,0 +1,16 @@
+
+
+
+ {#snippet definition()}
+
+ Category:
+
+ {data.morphism.category_name}
+
+
+ {/snippet}
+
diff --git a/src/routes/morphisms/+page.server.ts b/src/routes/morphisms/+page.server.ts
new file mode 100644
index 00000000..0825b73e
--- /dev/null
+++ b/src/routes/morphisms/+page.server.ts
@@ -0,0 +1,5 @@
+import { fetch_structures_and_tags } from '$lib/server/fetchers/structures'
+
+export const load = () => {
+ return fetch_structures_and_tags('morphism')
+}
diff --git a/src/routes/morphisms/+page.svelte b/src/routes/morphisms/+page.svelte
new file mode 100644
index 00000000..f94edcfc
--- /dev/null
+++ b/src/routes/morphisms/+page.svelte
@@ -0,0 +1,7 @@
+
+
+
diff --git a/src/routes/morphisms/[tag]/+page.server.ts b/src/routes/morphisms/[tag]/+page.server.ts
new file mode 100644
index 00000000..7624ca36
--- /dev/null
+++ b/src/routes/morphisms/[tag]/+page.server.ts
@@ -0,0 +1,12 @@
+import type { EntryGenerator } from './$types'
+import { fetch_tagged_structures } from '$lib/server/fetchers/structures'
+import { fetch_structure_tags } from '$lib/server/fetchers/tags'
+
+export const entries: EntryGenerator = () => {
+ return fetch_structure_tags('morphism')
+}
+
+export const load = (event) => {
+ const tag = event.params.tag
+ return fetch_tagged_structures('morphism', tag)
+}
diff --git a/src/routes/morphisms/[tag]/+page.svelte b/src/routes/morphisms/[tag]/+page.svelte
new file mode 100644
index 00000000..d3340462
--- /dev/null
+++ b/src/routes/morphisms/[tag]/+page.svelte
@@ -0,0 +1,7 @@
+
+
+