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.

`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.
```

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!

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

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.
```

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

Last updated: Jun 23 2024 at 04:03 UTC