From 9a439d4a4e2b1ce262e200431848cf34014b418f Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 7 Aug 2015 14:39:45 +0200 Subject: [PATCH] feat(library.md): update reference to classical axiom --- library/library.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/library.md b/library/library.md index 874b5448a..727191ab0 100644 --- a/library/library.md +++ b/library/library.md @@ -27,8 +27,8 @@ The `standard` library does not rely on any axioms beyond this framework, and is hence constructive. It includes theories of the natural numbers, integers, lists, and so on. -The `classical` library imports the law of the excluded middle, choice functions, -and propositional extensionality. See `logic/axioms` for details. +The `classical` library also imports a choice function axiom, which implies +the law of the excluded middle and propositional extensionality. See [logic.choice](logic/choice.lean) for details. See also the [hott library](../hott/hott.md), a library for homotopy type theory based on a predicative foundation.