|0.2.2||Mar 23, 2022|
|0.2.1||Mar 23, 2022|
|0.2.0||Mar 23, 2022|
|0.1.0||Mar 23, 2022|
#1339 in Math
23 downloads per month
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:
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) -> ...] <=> ....
c is wrong relative to
so, Caso corrects this to
(a -> b)[(a <- c) -> ...] <=> ....
Higher morpisms are supported by counting
- (1) and
= (2) in the arrow.
<-> is a 1-isomorphism and
<=> is a 2-isomorphism.
How to solve triangles
Triangles can be expanded into commutative square using identity morphisms.
> (A <-> B)[(A -> C) -> (B -> C)] <=> (C -> C) (A <-> B)[(A -> C) -> (B -> C)] <=> (C <-> C)
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.