From c690a68ba0b78b913cbcb60f7508d431071d4c79 Mon Sep 17 00:00:00 2001 From: Vincent Semeria Date: Fri, 4 Oct 2019 18:29:58 +0200 Subject: Replace classical reals quotient axioms by functional extensionality. Define homotopy propositions and homotopy sets. Rename local variable R in test Nsatz, to avoid a name collision with the type of real numbers. --- doc/changelog/10-standard-library/10827-dedekind-reals.rst | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 doc/changelog/10-standard-library/10827-dedekind-reals.rst (limited to 'doc/changelog') diff --git a/doc/changelog/10-standard-library/10827-dedekind-reals.rst b/doc/changelog/10-standard-library/10827-dedekind-reals.rst new file mode 100644 index 0000000000..5d8467025b --- /dev/null +++ b/doc/changelog/10-standard-library/10827-dedekind-reals.rst @@ -0,0 +1,11 @@ +- New module `Reals.ClassicalDedekindReals` defines Dedekind real numbers + as boolean-values functions along with 3 logical axioms: limited principle + of omniscience, excluded middle of negations and functional extensionality. + The exposed type :g:`R` in module :g:`Reals.Rdefinitions` is those + Dedekind reals, hidden behind an opaque module. + Classical Dedekind reals are a quotient of constructive reals, which allows + to transport many constructive proofs to the classical case. + + See `#10827 `_, by Vincent Semeria, + based on discussions with Guillaume Melquiond, Bas Spitters and Hugo Herbelin, + code review by Hugo Herbelin. -- cgit v1.2.3