Igor wrote:

> **Puzzle 140**: Prove that any morphism has at most one inverse.

> Let \\(g: y \to x\\) to be an inverse of \\(f: x \to y\\), and \\(h: y \to x\\) to be another inverse of \\(f\\). In this case we have the right inverse condition hold for both:

> \[ f \circ g = 1_y \]

> \[ f \circ h = 1_y \]

> This implies that

> \[ f \circ g = f \circ h \]

> Composing both sides with \\(g\\) gives

>\[ g \circ f \circ g = g \circ f \circ h \]

> Using left inverse condition, \\(g \circ f = 1_x\\), we get

> \[1_x \circ g = 1_x \circ h\]

>\[ g = h \]

Great! You have proven that any two inverses of a given morphism are equal.

> So all inverses of a given function are equal (isomorphic?) to each other, so we can say that such inverse is unique (up to isomorphism?).

You're not being bold enough here: you're not extracting all the wisdom available from your actual argument. You proved any two inverses of a given morphism _in any category_ are _equal_ to each other. So you don't need to say "function" here, and you don't need to say "isomorphic", or "up to isomorphism".

In fact, we haven't even discussed what it _means_ for two functions to be isomorphic, or for morphisms in a category to be isomorphic, so it's probably wisest at this point to avoid saying such things.

> It also seems that having left and right inverses together form a universal property (I'm still not quite sure what are these exactly), which uniquely identifies the inverse of a given function.

"Being the inverse of \\(f\\)" is a property that uniquely identifies a function if such a function exists - that's what you showed.

A universal property is fancier. It's a property of an object in a category that identifies it _uniquely up to isomorphism_. But we haven't talked about those yet.

> **Puzzle 140**: Prove that any morphism has at most one inverse.

> Let \\(g: y \to x\\) to be an inverse of \\(f: x \to y\\), and \\(h: y \to x\\) to be another inverse of \\(f\\). In this case we have the right inverse condition hold for both:

> \[ f \circ g = 1_y \]

> \[ f \circ h = 1_y \]

> This implies that

> \[ f \circ g = f \circ h \]

> Composing both sides with \\(g\\) gives

>\[ g \circ f \circ g = g \circ f \circ h \]

> Using left inverse condition, \\(g \circ f = 1_x\\), we get

> \[1_x \circ g = 1_x \circ h\]

>\[ g = h \]

Great! You have proven that any two inverses of a given morphism are equal.

> So all inverses of a given function are equal (isomorphic?) to each other, so we can say that such inverse is unique (up to isomorphism?).

You're not being bold enough here: you're not extracting all the wisdom available from your actual argument. You proved any two inverses of a given morphism _in any category_ are _equal_ to each other. So you don't need to say "function" here, and you don't need to say "isomorphic", or "up to isomorphism".

In fact, we haven't even discussed what it _means_ for two functions to be isomorphic, or for morphisms in a category to be isomorphic, so it's probably wisest at this point to avoid saying such things.

> It also seems that having left and right inverses together form a universal property (I'm still not quite sure what are these exactly), which uniquely identifies the inverse of a given function.

"Being the inverse of \\(f\\)" is a property that uniquely identifies a function if such a function exists - that's what you showed.

A universal property is fancier. It's a property of an object in a category that identifies it _uniquely up to isomorphism_. But we haven't talked about those yet.