I’ve run into a problem with giving semantics to categorical programming languages.

Associativity of composition makes reduction relations icky.

A toy example to illustrate the problem (my real code uses actual typing judgments.)

The basic grammar

```
Inductive obj := unit | empty | prod (_ _: obj) | sum (_ _: obj).
Inductive term : sort -> sort -> Type :=
| id A: term A A
| compose {A B C}: term B C -> term A B -> term A C
| bang A: term A unit
| fanout {A B C}: term C A -> term C B -> term C (prod A B)
| fst {A B}: term (prod A B) A
| snd {A B}: term (prod A B) B
| absurd A: term empty A
| fanin {A B C}: term A C -> term B C -> term (sum A B) C
| inl {A B}: term A (sum A B)
| inr {A B}: term B (sum A B)
.
Infix "'o'" := compose (at level 30, no associativity).
```

You’d want to attach reduction relations like

```
Induction step: forall {A B}, term A B -> term A B -> Type :=
| step_id_left {A B} (f: term A B): id A o f ~> f
| step_id_right {A B} (f: term A B): f o id A ~> f
| step_fst_fanout {A B C} (f: term C A) (g: term C B): fst o fanout f g ~> f
| step_fanin_inl {A B C} (f: term A C) (g: term B C): fanin f g o inl ~> f
where "A ~> B" := (step A B).
```

And so on and so forth.

But there is a problem `(fst o fst) o fanout x y`

does not reduce

I could add a rule like

`| step_assoc {A B C D} (f: term C D) (g: term B C) (h: term A B): f o (g o h) ~> (f o g) o h`

But that would prefer one canonical form over the other. I want to make `f o (g o h)`

equivalent and not prefer one over the other. Also I would have to rework sum types.

I’m not quite sure what the recommended way of doing this is.

If Coq had higher inductive types one could add a loop to the AST.

`| compose_assoc {A B C D} (f: term C D) (g: term B C) (h: term A B): f o (g o h) = (f o g) o h`

And I feel like things would mostly just work.

But I’m not sure how to handle things rn.

You end up with some nonsense like:

`| compose {A B}: tree A B -> term A B`

Where tree would be something like a binary search tree thing/free path category.

And you would have various union operations combining trees together.

It just all seems very awkward in practice and I’m wondering if there is a better way for this sort of thing.