verify-commutativity
Generate first-order logic statements to verify categorical diagram commutativity by comparing two paths between objects. Use when you need to prove path equality in category theory.
Instructions
Verify that a categorical diagram commutes by generating FOL premises and conclusion.
When to use: You have a categorical diagram and want to verify path equality. When NOT to use: For non-categorical reasoning (use prove directly).
Example: path_a: ["f", "g"], path_b: ["h"] object_start: "A", object_end: "C" → Generates premises/conclusion for proving compose(f,g) = h
Output: Returns premises and conclusion to pass to the prove tool.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| path_a | Yes | List of morphism names in first path | |
| path_b | Yes | List of morphism names in second path | |
| object_start | Yes | Starting object | |
| object_end | Yes | Ending object | |
| with_category_axioms | No | Include basic category theory axioms (default: true) | |
| verbosity | No | Response verbosity: 'minimal' (token-efficient), 'standard' (default), 'detailed' (debug info) |