csw-derive 0.1.0

# csw-derive

Type system derivation engine for the **Categorical Semantics Workbench**.

This crate implements the Curry-Howard-Lambek correspondence as an automated construction: given a categorical structure specification, it derives the corresponding type system with typing rules, reduction rules, and structural properties.

## Overview

The derivation process transforms categorical structures into type systems:

| Categorical Structure | Derived Type System |
|-----------------------|---------------------|
| Terminal object | Unit type (1) |
| Products (A × B) | Pair types with fst/snd |
| Coproducts (A + B) | Sum types with case |
| Exponentials (B^A) | Function types (A → B) |
| Tensor (A ⊗ B) | Linear pairs |
| Linear hom (A ⊸ B) | Linear functions |

## Usage

```rust
use csw_core::CategoryBuilder;
use csw_derive::Deriver;

// Define a Cartesian Closed Category
let ccc = CategoryBuilder::new("STLC")
    .with_base("Int")
    .with_base("Bool")
    .with_terminal()
    .with_products()
    .with_exponentials()
    .cartesian()
    .build()
    .unwrap();

// Derive the type system
let type_system = Deriver::derive(&ccc);

// Print the derived type system
println!("{}", type_system);
```

## Derived Outputs

A `TypeSystem` contains:

- **Type constructors**: How to form types (Unit, Product, Arrow, etc.)
- **Term constructors**: How to form terms (variables, pairs, lambdas, etc.)
- **Typing rules**: Inference rules for type checking
- **Reduction rules**: β-reduction rules for evaluation
- **Equivalence rules**: η-expansion rules
- **Structural rules**: Weakening, contraction, exchange

## Example Output

For a CCC specification, the derivation produces:

```
Types:
  τ ::= Int | Bool | 1 | τ × τ | τ → τ

Terms:
  e ::= x | () | (e, e) | fst e | snd e | λx.e | e e

Typing Rules:
  Γ ⊢ () : 1                              (unit-intro)
  Γ ⊢ a : A    Γ ⊢ b : B
  ────────────────────────                (pair-intro)
  Γ ⊢ (a, b) : A × B
  ...

Structural Rules:
  Weakening:   ✓
  Contraction: ✓
  Exchange:    ✓
```

## License

Licensed under either of Apache License, Version 2.0 or MIT license at your option.