The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

If I have

[Definition foo : bar.]

and I have a type [baz] which is convertible with [bar] (for example, if I have [baz := bar]), is it possible to get Coq to replace [foo] with the equivalent

[Definition foo : baz.]

?

More specifically, I have the following definition:

Set Implicit Arguments.

Set Printing All.

Set Printing Universes.

Record Category (obj : Type) (mor : obj -> obj -> Type) := {

  Object :> _ := obj;

  Morphism := mor : Object -> Object -> _;

  

  Identity : forall o, Morphism o o;

  Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d';

  

  Associativity : forall o1 o2 o3 o4 (m1 : Morphism o1 o2) (m2 : Morphism o2 o3) (m3 : Morphism o3 o4),

    Compose (Compose m3 m2) m1 = Compose m3 (Compose m2 m1);

  LeftIdentity : forall a b (f : Morphism a b), (Compose (Identity b) f) = f;

  RightIdentity : forall a b (f : Morphism a b), (Compose f (Identity a)) = f

}.

and my goal is to make

Check (@Category nat (fun _ _ => unit)).

give me [Set].  I can do this by removing the [Morphism := ] line, and renaming [mor] to [Morphism].  However, it's useful to be able to identify things as [Morphisms], so that, for example, when I have a bunch of hypotheses, the morphisms carry around the information of their source and destination, so that I can [Compose] them, and don't have to figure out that information in order to compose them, and also so that I can make tactics which act specifically on [Morphism]s.

So my current idea is to remove the [Morphism := ] from the record definition, define [Morphism] myself later, and then I want to change the types of [Identity], [Compose], etc., so that the talk about [Morphism] rather than [mor].  Is there a way to do this, or another way to get around the extra [Type] introduced by [Morphism := mor;]?

Thanks.

-Jason