Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Proving eq_dep statements?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proving eq_dep statements?


chronological Thread 
  • From: Daniel Schepler <dschepler AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Cc: ben <Benedikt.Ahrens AT unice.fr>
  • Subject: Re: [Coq-Club] Proving eq_dep statements?
  • Date: Fri, 10 Sep 2010 10:45:06 -0700
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=from:to:subject:date:user-agent:cc:references:in-reply-to :mime-version:content-type:content-transfer-encoding:message-id; b=HAQ6UDTe/BFH9vdsNPMt+GdOZgSJfd1/YtKDRY2kPMKNFJjsIcPsSROZgVCIip2zTN 9jOu9x7z+9LJCBAP0Bvrb+s8AdvNnUNSRTCM32nFhhh6BlnG0FLdNbPJBZ2R9gMnSMBZ g2Uo9lwoOK8KnATjntVjkgqQMwlYMy1gyRszQ=

On Friday 10 September 2010 09:25:15 ben wrote:
> Are you using a setoidal equality on morphisms as in ConCaT ?

No, I'm using Leibniz equality there too.  My thought was that if I ever 
wanted a category like topological spaces with homotopic continuous functions 
being identified, I'd just feed quotients in as the morphism types.
-- 
Daniel Schepler



Archive powered by MhonArc 2.6.16.

Top of Page