Here is the essence of a problem I have run in to: I have a finite poset D with a terminal object. If I formally invert all of the morphisms, and add these into my diagram, does the new diagram D' still commute?

I think that the resulting diagram will still commute basically because I have done a lot of examples. Working out a few examples you can see that it basically follows by doing it for the "commutative triangle", and applying this finitely many times. It feels like I should be able to do some kind of messy induction, but I do not really want such a proof cluttering up my work.

Is there a reference I could quote for a result like this? It seems like if it is true it should be a "folk lemma".

Of course, if you have more relaxed criteria for when the result will hold, that would be helpful too.

Also if you know of a conceptual proof which does not fall back on some messy induction, that would be wonderful!

EDIT: An example might help to clarify my question. (How do you draw diagrams on MO?)

```
a-->b
^ ^
| |
c-->d
```

is my poset. b is the terminal object. Now say someone told you that this was actually a subcategory of a larger category, and in that larger category all of the arrows were invertible. Now consider the larger diagram consisting of the 4 original arrows and their inverses. Is this diagram also commutative? Yes! It is just one or two lines of formal manipulation.