Stream: Coq users

Topic: Identity Morphism is Unique


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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