The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Which version of Coq are you using?  In 8.4beta2, [f_equal] finishes the proof for you.  Alternatively, in 8.4beta2, you can do [change (fun x y : Obj => Hom x y) with Hom], though I don't think 8.3 implements eta conversion.

In 8.3.... I'm not sure if there's a good way to do it.  You could prove [(fun x y : Obj => Hom x y) = Hom] by [functional_extensionality_dep] (from [FunctionalExtensionality]), and then use [JMeq_eq] (in [JMeq]) to say that you can prove [JMeq  C Op(Op(C))] instead of [eq C Op(Op(C))], and then you can rewrite on one side of the equation at a time.

Another way to do it is to do something like

Require Import JMeq.

Local Infix "~=" := JMeq (at level 70).

Definition Obj (C : Cat) := match C with MkCat Obj _ _ => Obj end.

Definition HomT (C : Cat) : { A : Type & A }.

  destruct C.

  exact (existT _ _ Hom).

Defined.

Definition Hom C : projT1 (HomT C) := projT2 (HomT C). 

Definition IdT (C : Cat) : { A : Type & A }.

  destruct C.

  exact (existT _ _ Id).

Defined.

Definition Id C : projT1 (IdT C) := projT2 (IdT C).

Lemma cat_eq (C C' : Cat) : Obj C = Obj C' -> Hom C ~= Hom C' -> Id C ~= Id C' -> C = C'.

  destruct C, C'.

  intros; simpl in *; repeat subst.

  unfold Hom, Id, HomT, IdT in *.

  simpl in *.

  repeat subst.

  reflexivity.

Qed.

and then [apply cat_eq].  Although if you're going to do that, you might want to use a [Record], like

Record Cat := {

  Obj : Type;

  Hom : Obj -> Obj -> Set; 

  Id : forall x : Obj, Hom x x

  }.

which defined [Obj] and [Hom] and [Id] for you.

-Jason

On Tue, Jul 17, 2012 at 4:02 PM, Alexander Katovsky <apk32 AT cam.ac.uk> wrote:

Inductive Cat : Type :=
  MkCat : forall (Obj : Type)
                 (Hom : (Obj -> Obj -> Set))
                 (Id : forall x : Obj, Hom x x), Cat.

Definition Op (x : Cat) : Cat :=
  match x with
    MkCat Obj Hom Id => (MkCat Obj (fun x y => Hom y x) Id)
  end.

Lemma OpOp: forall C, C = Op(Op(C)).
  unfold Op.
  intro C.
  case C; simpl.
  intros Obj Hom Id.
  f_equal.
  intros H_Obj H_Hom H_Id.
  dependent rewrite <- H_Hom.