## Stream: Coq users

### Topic: Identity Morphism is Unique

#### Fabian Beuke (Sep 18 2023 at 12:07):

I try to create the following proof in Coq https://proofwiki.org/wiki/Identity_Morphism_is_Unique

``````Section Category.
Variable Obj : Type.
Variable Hom : Obj -> Obj -> Type.

Variable id : forall (X : Obj), Hom X X.
Variable comp : forall (X Y Z : Obj), Hom X Y -> Hom Y Z -> Hom X Z.

Hypothesis id_left : forall (X Y : Obj) (f : Hom X Y), comp (id X) f = f.
Hypothesis id_right : forall (X Y : Obj) (f : Hom X Y), comp f (id Y) = f.

Theorem identity_unique : forall (X : Obj) (id1 id2 : Hom X X),
(forall (Y : Obj) (f : Hom X Y), comp id1 f = f) ->
(forall (Y : Obj) (f : Hom X Y), comp id2 f = f) ->
id1 = id2.
Proof.
intros X id1 id2 Hid1 Hid2.
rewrite <- (Hid1 X (id1)).
rewrite (Hid2 X (id1)).
reflexivity.
Qed.
End Category.
``````

This is what I have got so far. But I get the following error: The term "id X" has type "Hom X X" while it is expected to have type "Obj".

I assume the error is trivial, but I'm a total beginner in Coq, so I would appreciate any help to fix this proof.

#### Paolo Giarrusso (Sep 18 2023 at 12:18):

`comp` takes three object arguments before the arrow, so for instance this works:

``````  Hypothesis id_left : forall (X Y : Obj) (f : Hom X Y), comp X X Y (id X) f = f.
``````

But those arguments can be inferred, so underscores work:

``````  Hypothesis id_left : forall (X Y : Obj) (f : Hom X Y), comp _ _ _ (id X) f = f.
``````

or you can make those arguments implicit, then your example will typecheck:

``````  Variable comp : forall {X Y Z : Obj}, Hom X Y -> Hom Y Z -> Hom X Z.

Hypothesis id_left : forall (X Y : Obj) (f : Hom X Y), comp (id X) f = f.
``````

#### Paolo Giarrusso (Sep 18 2023 at 12:23):

that proof didn't quite work yet — I have a working version I can post. I don't want to spoil the exercise, but in my solution I needed more selective rewriting; after adding `From Coq Require Import Setoid.`, one can use `rewrite equality at N`— for instance,

``````  Theorem identity_unique : forall (X : Obj) (id1 id2 : Hom X X),
(forall (Y : Obj) (f : Hom X Y), comp id1 f = f) ->
(forall (Y : Obj) (f : Hom X Y), comp id2 f = f) ->
id1 = id2.
Proof.
intros X id1 id2 Hid1 Hid2.
rewrite <- (Hid1 X (id1)).
rewrite <-(Hid2 X (id1)) at 2.
``````

Here the `rewrite` works — the proof isn't quite right yet but your link should have enough hints for you to try more!

#### Fabian Beuke (Sep 18 2023 at 12:26):

Thank you, Paolo. Your assistance has been helpful. With the information you've provided, I think I can now proceed.

#### Fabian Beuke (Sep 19 2023 at 13:32):

Hi Paolo,

i managed to fix both issues. This is how my proof looks right now. What do you think?

``````Section Category.
Variable Obj : Type.
Variable Hom : Obj -> Obj -> Type.

Variable id : forall (X : Obj), Hom X X.
Variable comp : forall {X Y Z : Obj} , Hom Y Z -> Hom X Y -> Hom X Z.

Hypothesis id_left : forall {X Y : Obj} (f : Hom X Y), comp f (id X) = f.
Hypothesis id_right : forall {X Y : Obj} (f : Hom X Y), comp (id Y) f = f.

Theorem identity_unique : forall (X : Obj) (id1 id2 : Hom X X),
(forall (Y : Obj) (f : Hom X Y), comp f id1 = f) ->
(forall (Y : Obj) (f : Hom X Y), comp f id2 = f) ->
id1 = id2.

Proof.
intros X id1 id2 Hid1 Hid2.
(* By Hid1, we know comp (id X) id1 = id X *)
assert (comp (id X) id1 = id X) as Htemp1 by (apply Hid1).
(* By Hid2, we know comp (id X) id2 = id X *)
assert (comp (id X) id2 = id X) as Htemp2 by (apply Hid2).
transitivity (comp (id X) id1).
- symmetry.
apply id_right.
- symmetry.
transitivity (comp (id X) id2).
+ symmetry.
apply id_right.
+ rewrite Htemp1.
symmetry.
symmetry.
rewrite Htemp2.
reflexivity.
Qed.
End Category.
``````

#### Paolo Giarrusso (Sep 19 2023 at 21:01):

that makes sense! "symmetry. symmetry." can likely be dropped, right?

Last updated: Jun 23 2024 at 04:03 UTC