moonlight-category

Part of Moonlight, the sheaf-theoretic computation layer beneath Melusine and Pale Meridian.

moonlight-category is Moonlight's categorical tier. Building on moonlight-core, it provides a totalised, explicit-error category abstraction together with the finite, runtime-validated categories and site/path presentations the compiler uses to model its own structure.

Relationship to data-category

If you want general indexed category theory in Haskell, prefer Sjoerd Visscher's data-category. Its typed-arrow calculus is the primary inspiration for this package's indexed layer, and several modules under Moonlight.Category.Indexed are adapted from it. Thank you to Sjoerd Visscher for the design and implementation work in data-category.

Full attribution and the upstream BSD-3-Clause license are recorded in THIRD_PARTY_NOTICES.md.

What it provides

• A category abstraction. The Category class is totalised: objects, morphisms, 2-morphisms, compositors and a category-specific error type are associated types, and every operation returns Either.
• Limits and colimits. A class tower for products, coproducts, pullbacks, pushouts, equalizers and coequalizers.
• Higher structure. 2-categories, bicategories, monoidal and enriched categories.
• Finite categories. FinCat: runtime-validated finite categories with handles, bit-packed thin variants, composable chains and core/automorphism groupoid extraction.
• Finite-category presentations. Moonlight.Category.Presentation provides a focused authoring EDSL for finite posets and fully enumerated finite categories, compiling down to validated FinCat.
• Sites and presentations. Site manifests with validation, reachable-closure and import-cycle diagnostics, path categories, quotients, and compilation down to FinCat.
• Rewriting witnesses. Adhesive and PBPO pushout-complement witnesses, structured cospans, double categories, and decorated composition/presentation.
• Indexed category theory. The typed-arrow layer adapted from data-category.
• Simplicial substrate. Runtime-dimensional Δ morphisms, finite truncated simplicial sets, standard/boundary/horn spaces, nerves, Kan interfaces, and connected-component/core-groupoid queries over finite composable categories.

Public modules

Module	Cabal component	Surface
Moonlight.Category	moonlight-category	The broad categorical surface: Category and composition, the limit/colimit and higher-category towers, finite and thin categories, invertibility/groupoids, adhesive & PBPO witnesses, structured cospans, double categories, decorated composition, Galois connections, polynomial functors, covering families, and the site/path layer.
Moonlight.Category.Indexed	moonlight-category	The indexed, typed-arrow category-theory layer adapted from data-category: indexed categories, functors, natural transformations, adjunctions, (co)limits, Kan extensions, products/coproducts and the simplex category.
Moonlight.Category.Presentation	moonlight-category	The finite-category authoring surface: named objects, named nonidentity morphisms, strict-order below declarations, identities in equations, and compilation to FinCat.
Moonlight.Category.Notation	moonlight-category	Scoped query and composition helpers for already-compiled FinCat values.
Moonlight.Category.Simplicial	moonlight-category:simplicial	The public simplicial surface: Δ, simplicial sets, nerves, Kan interfaces, homotopy queries, and pure validation.

The Moonlight.Category.Pure.* leaves live in named implementation sublibraries: abstract for generic category theory, finite for FinCat/presentation runtime, site for site and path compilation, indexed for the adapted data-category typed-arrow layer, and simplicial for Δ, simplicial sets, nerves and Kan interfaces. Effectful law harnesses and cross-package test fixtures live in the laws sublibrary rather than the pure production components.

Main-library and simplicial consumers

The simplicial facade is a separate public Cabal component. A program using both facades must request both components explicitly:

build-depends:
    moonlight-category >= 1.1.0.0 && < 1.2,
    moonlight-category:simplicial >= 1.1.0.0 && < 1.2

import Moonlight.Category
import Moonlight.Category.Simplicial

Those two facades are the ordinary consumer path. Moonlight.Category owns site compilation and provenance lookup; Moonlight.Category.Simplicial owns nerves and their simplicial queries. A consumer should not need a Pure.* import to compile a site's import category, inspect its nerve, or recover source object names.

Site provenance and nerves

Use thinSiteImportKernel when only the import category is required, then obtain its FinCat with thinSiteKernelCodomain. Use thinSiteKernel when full cover validation is required. Site-derived FinObjectId values are kernel-relative representation tokens: their numerical order is not a semantic name or a stable persistence contract. Preserve the ThinSiteKernel and cross the boundary through thinSiteFinObject and thinSiteObjectValue instead of reconstructing an object map from siteObjects.

For ordinary topological or combinatorial work, use normalizedNerve; it enumerates nonidentity chains and closes under faces. unnormalizedNerve materializes every composable chain, including identity insertions, and is deliberately for small law or diagnostic workloads: its truncation bound is not a memory budget. A validated ComposableChain retains its vertices, so chainVertices is a total projection; there is no fallible category lookup after construction.

Dependency footprint

Hackage's package-level dependency summary aggregates dependencies from every component in the distribution. Depending on the main moonlight-category library does not select moonlight-category:laws and therefore does not add Tasty, Hedgehog, or moonlight-pale:test-laws. Consumers opt into that reusable law harness explicitly with a dependency on moonlight-category:laws.

Finite-category presentations

Use Moonlight.Category.Presentation to write finite categories declaratively. Compilation always produces the validated runtime representation FinCat.

Finite posets

below declares strict generating inequalities. Compilation takes the transitive closure, rejects cycles, and supplies identities implicitly.

import Moonlight.Category.Presentation

threeChain :: Either FinCatBuildError FinCat
threeChain =
  finCategory $ do
    [a, b, c] <- objects ["A", "B", "C"]
    below a b
    below b c

Fully enumerated finite categories

In the general dialect, each call to arrow declares one actual nonidentity morphism of the resulting category. Equations determine the nonidentity composition table.

import Moonlight.Category.Presentation

commutingTriangle :: Either FinCatBuildError FinCat
commutingTriangle =
  finCategory $ do
    a <- object "A"
    b <- object "B"
    c <- object "C"

    f <- arrow a b "f"
    g <- arrow b c "g"
    h <- arrow a c "h"

    equate (g `after` f) h

Identities may be named inside equations:

inversePair :: Either FinCatBuildError FinCat
inversePair =
  finCategory $ do
    a <- object "A"
    b <- object "B"

    f <- arrow a b "f"
    g <- arrow b a "g"

    equate (g `after` f) (identityAt a)
    equate (f `after` g) (identityAt b)

Longer paths are accepted when their proper intermediate composites are determined elsewhere in the presentation. Equation declaration order is irrelevant.

The presentation dialect accepts declared morphisms and equations over determined composites. An equation such as equate f g for distinct declared morphisms is rejected rather than silently identifying them.

For querying and composing morphisms after compilation, import Moonlight.Category.Notation separately.

Acknowledgements

The representation of finite and finitely-presented categories as concrete, runtime-validated data structures, including FinCat and the site/path presentations that compile down to it, was directly inspired by the AlgebraicJulia ecosystem and the work on attributed C-sets (acsets), whose thesis is precisely that categorical objects can be realised as performant data structures. The implementation here is independent; the conceptual debt is real and gratefully acknowledged.

Evan Patterson, Owen Lynch, and James Fairbanks. "Categorical Data Structures for Technical Computing." arXiv:2106.04703. https://arxiv.org/abs/2106.04703

Thank you to Evan Patterson, Owen Lynch, James Fairbanks, and the AlgebraicJulia community.

License

Moonlight's original code is licensed under MIT; see LICENSE. The indexed modules adapted from data-category remain BSD-3-Clause; their copyright notice, license terms, and attribution are recorded in THIRD_PARTY_NOTICES.md.

cabal install moonlight-category