Crate csw_core 

csw-core

Core categorical structures for the Categorical Semantics Workbench.

This crate provides the foundational types for specifying categorical structures (products, coproducts, exponentials, tensor products, etc.) and their properties. From these specifications, type systems can be automatically derived using the Curry-Howard-Lambek correspondence.

Overview

The Categorical Semantics Workbench operationalizes the insight that:

• Logic ↔ Type Theory ↔ Category Theory

Given a categorical structure, we can mechanically derive the corresponding type system, and vice versa.

Example

use csw_core::CategoryBuilder;

// Define a Cartesian Closed Category (CCC)
// This will derive the Simply-Typed Lambda Calculus
let ccc = CategoryBuilder::new("STLC")
    .with_base("Int")
    .with_base("Bool")
    .with_terminal()
    .with_products()
    .with_exponentials()
    .cartesian()
    .build()
    .expect("valid CCC specification");

Categorical Structures and Their Logics

Structure	Logic/Type System
Cartesian Closed Category	Simply-typed λ-calculus
Bicartesian Closed Category	λ-calculus with sums
Symmetric Monoidal Closed Category	Linear λ-calculus
Affine Category	Affine types (Rust-like)

Structs

BaseObject

A base/primitive object in the category.

CategoryBuilder

Builder for constructing categorical specifications.

CategorySpec

A specification of categorical structure.

StructuralFeatures

Structural features present in a category.

TensorSpec

Specification for monoidal tensor product.

Enums

Associativity

Associativity type for monoidal structure.

DiagonalSpec

Specification for diagonal morphism (contraction/copying).

TerminalSpec

Specification for terminal morphism (weakening/discarding).

ValidationError

Errors that can occur when building or validating a categorical specification.