inverse_map_uniq.v

Definition obj := Type.

Inductive map : Type :=
| Id : obj -> map
| Diff : obj -> obj -> map
| Comp : map -> map -> map.

Inductive hom : map -> obj -> obj -> Prop :=
| HomId : forall f a,
    f = Id a -> hom f a a
| HomDiff : forall f a b,
    f = Diff a b -> hom f a b
| HomComp : forall f g h a b c,
    f = Comp g h ->
    hom g a b ->
    hom h b c ->
    hom f a c.

Inductive map_eq : map -> map -> Prop :=
| Com : forall f g,
    map_eq f g -> map_eq g f
| Eq : forall f, map_eq f f
| CompAssoc : forall f g h,
    map_eq
      (Comp (Comp h g) f)
      (Comp h (Comp g f))
| IdL : forall a b f g,
    hom f a b ->
    map_eq (Comp (Id b) f) g ->
    map_eq f g
| IdR : forall a b f g,
    hom f a b ->
    map_eq (Comp f (Id a)) g ->
    map_eq f g.

Definition inverse a b f g :=
  hom f a b /\
  hom g b a /\
  Comp f g = Id b /\
  Comp g f = Id a.

Lemma inverse_uniq : forall a b (f g g' : map),
  inverse a b f g ->
  inverse a b f g' ->
  map_eq g g'.
Proof.
  intros.
  inversion H. clear H.
  inversion H0. clear H0.
  inversion H2. clear H2.
  inversion H3. clear H3.
  inversion H4. clear H4.
  inversion H5. clear H5.
  assert (map_eq (Comp (Comp g f) g')
                 (Comp g (Comp f g'))) by constructor.
  rewrite H6 in H5.
  rewrite H4 in H5.
  apply (IdL b a g' (Comp g (Id b)) H2) in H5.
  apply Com in H5.
  apply (IdR b a g g' H0) in H5.
  assumption.
Qed.