coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proving eq_dep statements?

From: David Leduc <david.leduc6 AT googlemail.com>
To: ben <Benedikt.Ahrens AT unice.fr>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Proving eq_dep statements?
Date: Sat, 11 Sep 2010 01:12:13 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=ryhlNYIk5Tt4ELVsPbz1Kx/osWDNcsl5IcuLPP0VUbmyT1/FZmADsoZol0rpC51Kmi zfn40VzeWC52rPtMttobFolU0yCmtS/SRSyM8hP9Oxr7aJR+aBxyDPbwIxn7Qdt9X965 gX5vyVGbd7U2FsOj8jU8Ls60WIhh+Lx1EBoU0=

Hi Ben,

> (You can find all of this in my lib of cats on
> http://math.unice.fr/~ahrens ;).

I had a look at it. It looks good.

Why do you split the definition of a category into first a class and
then a record?
Does it help with duplication of definitions?

[Coq-Club] Proving eq_dep statements?, Daniel Schepler
- Re: [Coq-Club] Proving eq_dep statements?, Adam Chlipala
  - Re: [Coq-Club] Proving eq_dep statements?, Vladimir Voevodsky
- Re: [Coq-Club] Proving eq_dep statements?, ben
  - Re: [Coq-Club] Proving eq_dep statements?, Daniel Schepler
    - Re: [Coq-Club] Proving eq_dep statements?, ben
      - Re: [Coq-Club] Proving eq_dep statements?, Daniel Schepler
      - Re: [Coq-Club] Proving eq_dep statements?, David Leduc
        
        Re: [Coq-Club] Proving eq_dep statements?, ben