refactor(library): set up and document standard/classical/hott imports

README.md

@@ -21,7 +21,7 @@ About
 - [To Do list](doc/todo.md)
 - [Authors](doc/authors.md)
 - [Tutorial](doc/lean/tutorial.org)
-- [Standard Library](library/standard.md)
+- [Library](library/library.md)
 
 Requirements
 ------------

library/classical.lean

@@ -0,0 +1,5 @@
+-- Copyright (c) 2014 Jeremy Avigad. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Jeremy Avigad
+
+import standard logic.axioms

library/hott/default.lean

@@ -0,0 +1,10 @@
+-- Copyright (c) 2014 Jeremy Avigad. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Jeremy Avigad
+
+-- hott.default
+-- ============
+
+-- A library for homotopy type theory
+
+import ..standard .path .equiv .trunc .fibrant

library/hott/hott.md

@@ -1,18 +1,19 @@
 standard.hott
 =============
 
-A library for Homotopy Type Theory, which avoid the use of prop. Many
-standard types are imported from `data`, but then theorems
-are proved about them using predicativee versions of the logical
-operations. For example, we use the path type, products, sums, sigmas,
-and the empty type, rather than equality, and, or, exists, and
-false. These operations take values in Type rather than Prop.
+A library for homotopy type theory. HoTT is consistent with the
+existence of an imprediative, proof irrelevant `Prop`, but favors
+"proof relevant," predicative versions of the usual logical
+constructions. For example, we use the path type, products, sums,
+sigmas, and the empty type, rather than equality, and, or, exists, and
+false. These operations take values in `Type` rather than `Prop`.
 
-We view Homotopy Theory Theory as compatible with the axiomatic
-framework of Lean, simply ignoring the impredicative, proof irrelevant
-Prop. This is o.k. as long as we do not import additional axioms like
-propositional extensionality or Hilbert choice, which are incompatible
-with HoTT.
+Note that the univalence axiom is inconsistent with classical axioms
+such as propositional extensionality or Hilbert choice, and we have to
+ensure that the library does not import these.
+
+The modules imported by the command `import hott` are found in the
+file [default](default.lean).
 
 * [path](path.lean) : the path type and operations on paths
 * [equiv](equiv.lean) : equivalence of types

library/library.md

@@ -0,0 +1,35 @@
+The Lean Library
+================
+
+The Lean library is contained in the following modules and directories:
+
+* [general_notation](general_notation.lean) : commonly shared notation
+* [logic](logic/logic.md) : logical constructs and axioms
+* [data](data/data.md) : concrete datatypes and type constructors
+* [struc](struc/struc.md) : axiomatic structures
+* [hott](hott/hott.md) : homotopy type theory
+* [tools](tools/tools.md) : additional tools
+
+Modules can be loaded individually, but they are also be loaded by importing the
+following packages:
+
+* [standard](standard.lean) : constructive logic and datatypes
+* [classical](classical.lean) : classical mathematics
+* [hott](hott/default.lean) : homotopy type theory
+
+Lean's default logical framework is a version of the Calculus of Constructions with:
+
+* an impredicative, proof-irrelevant type `Prop` of propositions
+* a non-cumulative hierarchy of universes, `Type 1`, `Type 2`, ... above `Prop`
+* inductively defined types
+
+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 `hott` library is compatible with the standard library, but favors "proof
+relevant" versions of the logical connectives, based on `Type` rather than
+`Prop`. See `hott` for details.

library/standard.lean

@@ -1,8 +1,10 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Leonardo de Moura
+-- Authors: Leonardo de Moura, Jeremy Avigad
 
--- changing to this breaks some tests:
--- import logic data tools.tactic
+-- standard
+-- ========
 
-import logic tools.tactic data.num data.string data.prod logic.connectives.cast
+-- The constructive core of Lean's library.
+
+import logic data tools.tactic

library/standard.md

@@ -1,12 +0,0 @@
-standard
-========
-
-The Lean standard library. By default, `import standard` does not
-import any axioms. See logic.axioms.
-
-* [general_notation](general_notation.lean) : notation shared by all libraries
-* [logic](logic/logic.md) : logical constructs and axioms
-* [data](data/data.md) : various datatypes
-* [struc](struc/struc.md) : axiomatic structures
-* [hott](hott/hott.md) : homotopy type theory
-* [tools](tools/tools.md) : various additional tools