The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is there a way to make [Existing Class] behave like [Class]?  For example, in the following code, if I have [Existing Class IsCat], then [rewrite Associativity] generates an extra goal [IsCat C]; but if I define [IsCat] to be a [Class] to start off with, then this goal does not show up.

Set Implicit Arguments.

Record Cat :=

  { 

    Object :> Type;

    Morphism : Object -> Object -> Type;

    Compose : forall {s d d'}, Morphism d d' -> Morphism s d -> Morphism s d'

  }.

Record IsCat (C : Cat) :=

  { 

    Associativity : forall o1 o2 o3 o4

                           (m1 : Morphism C o1 o2)

                           (m2 : Morphism C o2 o3)

                           (m3 : Morphism C o3 o4),

                      Compose C (Compose C m3 m2) m1 = Compose C m3 (Compose C m2 m1)

  }.

Existing Class IsCat.

Section foo.

  Variable C : Cat.

  Context `(IsCat C).

  Lemma foo o1 o2 o3 o4

        (m1 : Morphism C o1 o2)

        (m2 : Morphism C o2 o3)

        (m3 : Morphism C o3 o4)

  : Compose C (Compose C m3 m2) m1 = Compose C (Compose C m3 m2) m1.

    rewrite Associativity.

Thanks!

-Jason