# Crate caso

Expand description

## Caso

Category Theory Solver for Commutative Diagrams.

``````=== Caso 0.2 ===
> (A <-> B)[(A <-> C) -> (B <-> D)] <=> (C -> D)
(A <-> B)[(A <-> C) -> (B <-> D)] <=> (C <-> D)``````

To run Case from your Terminal, type:

`cargo install --example caso caso`

Then, to run:

`caso`

#### Syntax

A commuative diagram in Caso is written in the following grammar:

`<left>[<top> -> <bottom>] <=> <right>`

This syntax is based on the notation for Path Semantics.

Caso automatically corrects directional errors, e.g. when you type `(a -> b)[(c -> a) -> ...] <=> ...`. the `c` is wrong relative to `a`, so, Caso corrects this to `(a -> b)[(a <- c) -> ...] <=> ...`.

Higher morpisms are supported by counting `-` (1) and `=` (2) in the arrow. For example, `<->` is a 1-isomorphism and `<=>` is a 2-isomorphism.

MorphismNotation
Directional`->`
Reverse Directional`<-`
Epi`->>`
Reverse Epi`<<-`
Mono`!->`
Reverse Mono`<-!`
Right Inverse`<->>`
Left Inverse`<<->`
Epi-Mono`!->>`
Reverse Epi-Mono`<<-!`
Iso`<->`
Zero`<>`

#### How to solve triangles

Triangles can be expanded into commutative square using identity morphisms.

For example:

``````> (A <-> B)[(A -> C) -> (B -> C)] <=> (C -> C)
(A <-> B)[(A -> C) -> (B -> C)] <=> (C <-> C)``````

Here, `C -> C` is an identity morphism from `C` to itself.

#### Design

Caso uses Avalog as monotonic solver.

The Avalog rules are located in “assets/cat.txt”.

The automated theorem prover uses the following steps:

1. Parse expression
2. Construct commutative square
3. Expand knowledge about morphisms using rules for Category Theory
4. Analyze new knowledge and reintegrate it into the commutative square
5. Synthesize expression.

## Modules

Commutative diagram solver.

Parse syntax.

Data structure for symbols in Avalog solver.

## Enums

Stores Caso expression.

Represents a morphism.

## Functions

Converts string into expression (panics when format is invalid).

Directional e.g. `A -> B`.

Higher directional e.g. `A => B`.

Epi e.g. `A ->> B`.

Epi-mono e.g. `A !->> B`.

Higher epi-mono e.g. `A !=>> B`.

Higher epi e.g. `A =>> B`.

Iso e.g. `A <-> B`.

Higher iso e.g. `A <=> B`.

Mono e.g. `A !-> B`.

Higher mono e.g. `A !=> B`.

A path e.g. `X[Y]`.

Reverse epi-mono e.g. `A <<-! B`.

Reverse epi-mono e.g. `A <<=! B`.

Reverse mono e.g. `A <-! B`.

Higher reverse mono e.g. `A <=! B`.

Reverse right inverse e.g. `A <<-> B`.

Higher reverse right inverse e.g. `A <<=> B`.

Right inverse e.g. `A <->> B`.

Higher right inverse e.g. `A <=>> B`.

Solve a string.

Zero e.g. `A <> B`.

Higher zero.