Category Theory Solver for Commutative Diagrams.
=== Caso 0.2 ===
Type `help` for more information.
> (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
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 | <> |
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.
Caso uses Avalog as monotonic solver.
The Avalog rules are located in "assets/cat.txt".
The automated theorem prover uses the following steps:
- Parse expression
- Construct commutative square
- Expand knowledge about morphisms using rules for Category Theory
- Analyze new knowledge and reintegrate it into the commutative square
- Synthesize expression.