## caso

Category Theory Solver for Commutative Diagrams

### 4 releases

 0.2.2 Mar 23, 2022 Mar 23, 2022 Mar 23, 2022 Mar 23, 2022

#1339 in Math

MIT/Apache

41KB
832 lines

# 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.

Morphism Notation
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.

~330KB