(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 00000000..147aa72e
--- /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 00000000..8fc1e87a
--- /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 00000000..e07477ec
--- /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 00000000..5bad5ec7
--- /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 00000000..b34c8476
--- /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 00000000..b59058a1
--- /dev/null
+++ b/src/routes/functor-property/[id]/+page.server.ts
@@ -0,0 +1,32 @@
+import { decode_property_ID } from '$lib/commons/property.url'
+import type { FunctorPropertyDB } from '$lib/commons/types'
+import { query } from '$lib/server/db'
+import { render_nested_formulas } from '$lib/server/rendering'
+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 00000000..879b8f14
--- /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}
+
+
+
+
diff --git a/src/routes/functor/[id]/+page.server.ts b/src/routes/functor/[id]/+page.server.ts
new file mode 100644
index 00000000..35efd0f2
--- /dev/null
+++ b/src/routes/functor/[id]/+page.server.ts
@@ -0,0 +1,96 @@
+import type {
+ FunctorDB,
+ FunctorPropertyAssignment,
+ FunctorPropertyAssignmentDB,
+ FunctorPropertyShort,
+} from '$lib/commons/types'
+import { batch } from '$lib/server/db'
+import { render_nested_formulas } from '$lib/server/rendering'
+import { error } from '@sveltejs/kit'
+import sql from 'sql-template-tag'
+
+// remove code duplication with category detail page
+
+export const load = async (event) => {
+ const id = event.params.id
+
+ const { results, err } = await batch<
+ [
+ FunctorDB,
+ FunctorPropertyAssignmentDB & { is_satisfied: number },
+ FunctorPropertyShort,
+ ]
+ >([
+ sql`
+ SELECT
+ f.id, f.name, f.source, f.target, f.description, f.url,
+ cs.name as source_name, ct.name as target_name
+ FROM functors f
+ INNER JOIN categories cs ON cs.id = f.source
+ INNER JOIN categories ct ON ct.id = f.target
+ WHERE f.id = ${id}
+ `,
+ // properties
+ sql`
+ SELECT
+ fp.property_id AS id,
+ fp.is_satisfied,
+ fp.reason,
+ fp.is_deduced,
+ CASE
+ WHEN fp.is_satisfied = TRUE THEN p.prefix
+ ELSE pf.negation
+ END AS prefix
+ FROM functor_property_assignments fp
+ INNER JOIN functor_properties p ON p.id = fp.property_id
+ INNER JOIN prefixes pf ON pf.prefix = p.prefix
+ WHERE fp.functor_id = ${id}
+ ORDER BY fp.position, lower(fp.property_id)
+ `,
+ // unknown properties
+ sql`
+ SELECT
+ p.id,
+ p.prefix
+ FROM functor_properties p
+ WHERE NOT EXISTS (
+ SELECT 1 FROM functor_property_assignments
+ WHERE functor_id = ${id} AND property_id = p.id
+ )
+ ORDER BY lower(p.id)
+ `,
+ ])
+
+ if (err) error(500, 'Could not load functor')
+
+ const [functors, properties_db, unknown_properties] = results
+
+ if (!functors.length) error(404, `Could not find functor with ID '${id}'`)
+
+ const [functor] = functors
+
+ const satisfied_properties: FunctorPropertyAssignment[] = properties_db
+ .filter((obj) => obj.is_satisfied)
+ .map((p) => ({
+ id: p.id,
+ reason: p.reason,
+ is_deduced: Boolean(p.is_deduced),
+ prefix: p.prefix,
+ }))
+
+ const unsatisfied_properties: FunctorPropertyAssignment[] = properties_db
+ .filter((obj) => !obj.is_satisfied)
+ .map((p) => ({
+ id: p.id,
+ reason: p.reason,
+ is_deduced: Boolean(p.is_deduced),
+ prefix: p.prefix,
+ }))
+
+ return render_nested_formulas({
+ functor,
+ satisfied_properties,
+ unsatisfied_properties,
+ unknown_properties,
+ })
+}
diff --git a/src/routes/functor/[id]/+page.svelte b/src/routes/functor/[id]/+page.svelte
new file mode 100644
index 00000000..7d754dee
--- /dev/null
+++ b/src/routes/functor/[id]/+page.svelte
@@ -0,0 +1,123 @@
+
+
+
+
+{functor.name}
+
+
+
+
+ {@html functor.description}
+
+
+
+{#key functor.id}
+
+
+ Satisfied Properties
+
+ {#if category_detail_level.value === 'all'}
+ !p.is_deduced)}
+ description="Properties from the database"
+ type="functor"
+ />
+
+ p.is_deduced)}
+ description="Deduced properties"
+ type="functor"
+ />
+ {:else if category_detail_level.value === 'merged'}
+
+ {:else if category_detail_level.value === 'basic'}
+ !p.is_deduced)}
+ description="Properties from the database; further properties can be deduced."
+ type="functor"
+ />
+ {/if}
+
+
+
+ Unsatisfied Properties
+
+ {#if category_detail_level.value === 'all'}
+ !p.is_deduced)}
+ description="Properties from the database"
+ type="functor"
+ />
+
+ p.is_deduced)}
+ description="Deduced properties*"
+ type="functor"
+ />
+
+ *This also uses the deduced satisfied properties.
+ {:else if category_detail_level.value === 'merged'}
+
+ {:else if category_detail_level.value === 'basic'}
+ !p.is_deduced)}
+ description="Properties from the database; further properties can be deduced."
+ type="functor"
+ />
+ {/if}
+
+
Unknown properties
+
+
+
+{/key}
+
+
diff --git a/src/routes/functors/+page.server.ts b/src/routes/functors/+page.server.ts
new file mode 100644
index 00000000..38d47a53
--- /dev/null
+++ b/src/routes/functors/+page.server.ts
@@ -0,0 +1,16 @@
+import type { FunctorShort } from '$lib/commons/types'
+import { query } from '$lib/server/db'
+import { error } from '@sveltejs/kit'
+import sql from 'sql-template-tag'
+
+export const prerender = true
+
+export const load = async () => {
+ const { rows: functors, err } = await query(
+ sql`SELECT id, name FROM functors ORDER BY lower(name)`,
+ )
+
+ if (err) error(500, 'Functors could not be loaded')
+
+ return { functors }
+}
diff --git a/src/routes/functors/+page.svelte b/src/routes/functors/+page.svelte
new file mode 100644
index 00000000..db84cc5a
--- /dev/null
+++ b/src/routes/functors/+page.svelte
@@ -0,0 +1,21 @@
+
+
+
+
+
diff --git a/src/routes/missing/+page.svelte b/src/routes/missing/+page.svelte
index a6e875fb..b3d53c96 100644
--- a/src/routes/missing/+page.svelte
+++ b/src/routes/missing/+page.svelte
@@ -55,7 +55,7 @@
>are
inconsistent, this indicates that some
- implication is missing.
+ implication is missing.