coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [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
- Re: [Coq-Club] Proving eq_dep statements?,
Daniel Schepler
- Re: [Coq-Club] Proving eq_dep statements?,
Adam Chlipala
Archive powered by MhonArc 2.6.16.