coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] SDG in Coq

From: Michael Shulman <mshulman AT ucsd.edu>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] SDG in Coq
Date: Tue, 22 Nov 2011 07:44:04 -0800

Has anyone developed any synthetic differential geometry in Coq? I'm
imagining adding axioms such as the existence of a line object with
the Kock-Lawvere property, such as would be valid in the internal type
theory of a smooth topos.

Mike

[Coq-Club] SDG in Coq, Michael Shulman