From c09f1c4eafde26fc509252fed3aa0f7ce319d00a Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Wed, 4 Mar 2015 21:06:39 -0500 Subject: [PATCH] feat(*.md): create markdown files for HoTT library, update ones in standard library --- README.md | 1 + hott/algebra/algebra.md | 12 ++++++++ hott/algebra/category/category.md | 5 +++ hott/algebra/precategory/precategory.md | 9 ++++++ hott/hott.md | 20 ++++++++++++ hott/init/axioms/axioms.md | 6 ++++ hott/init/init.md | 41 +++++++++++++++++++++++++ hott/init/types/types.md | 9 ++++++ hott/types/eq.hlean | 2 +- hott/types/types.md | 15 +++++++++ library/algebra/algebra.md | 1 + library/algebra/category/category.md | 4 +-- library/library.md | 10 +++--- 13 files changed, 127 insertions(+), 8 deletions(-) create mode 100644 hott/algebra/algebra.md create mode 100644 hott/algebra/category/category.md create mode 100644 hott/algebra/precategory/precategory.md create mode 100644 hott/hott.md create mode 100644 hott/init/axioms/axioms.md create mode 100644 hott/init/init.md create mode 100644 hott/init/types/types.md create mode 100644 hott/types/types.md diff --git a/README.md b/README.md index f10461e7c7..8eb16217e3 100644 --- a/README.md +++ b/README.md @@ -24,6 +24,7 @@ About - Theorem Proving in Lean: [HTML](https://leanprover.github.io/tutorial/index.html), [PDF](http://leanprover.github.io/tutorial/tutorial.pdf) - [Authors](doc/authors.md) - [Standard Library](library/library.md) +- [HoTT Library](hott/hott.md) - [Short Tutorial](doc/lean/tutorial.org) - [To Do list](doc/todo.md) diff --git a/hott/algebra/algebra.md b/hott/algebra/algebra.md new file mode 100644 index 0000000000..07dc67c581 --- /dev/null +++ b/hott/algebra/algebra.md @@ -0,0 +1,12 @@ +algebra +======= + +* [binary](binary.hlean) : properties of binary operations +* [relation](relation.hlean) : properties of relations +* [group](group.hlean) +* [groupoid](groupoid.hlean) + +Subfolders: + +* [precategory](precategory/precategory.md) +* [category](category/category.md) diff --git a/hott/algebra/category/category.md b/hott/algebra/category/category.md new file mode 100644 index 0000000000..9d3581f7f3 --- /dev/null +++ b/hott/algebra/category/category.md @@ -0,0 +1,5 @@ +algebra.category +================ + +* [basic](basic.hlean) +* [constructions](constructions.hlean) diff --git a/hott/algebra/precategory/precategory.md b/hott/algebra/precategory/precategory.md new file mode 100644 index 0000000000..c1f6531b7b --- /dev/null +++ b/hott/algebra/precategory/precategory.md @@ -0,0 +1,9 @@ +algebra.precategory +=================== + +* [basic](basic.hlean) +* [functor](functor.hlean) +* [constructions](constructions.hlean) +* [iso](iso.hlean) +* [nat_trans](nat_trans.hlean) +* [yoneda](yoneda.hlean) diff --git a/hott/hott.md b/hott/hott.md new file mode 100644 index 0000000000..e1d4270de9 --- /dev/null +++ b/hott/hott.md @@ -0,0 +1,20 @@ +The Lean Homotopy Type Theory Library +===================================== + +The Lean homotopy type theory library is contained in the following +modules and directories: + +* [init](init/init.md) : constants and theorems needed for low-level system operations +* [types](types/types.md) : concrete datatypes and type constructors +* [algebra](algebra/algebra.md) : algebraic structures + +Lean's homotopy type theory kernel is a version of Martin-Löf Type Theory with: + +* universe polymorphism +* a non-cumulative hierarchy of universes, `Type 0`, `Type 1`, ... +* inductively defined types + +By default, the univalence axiom is declared on initialization. + +See also the [standard library](../library/library.md). + diff --git a/hott/init/axioms/axioms.md b/hott/init/axioms/axioms.md new file mode 100644 index 0000000000..6644bf5b3f --- /dev/null +++ b/hott/init/axioms/axioms.md @@ -0,0 +1,6 @@ +init.axioms +=========== + +* [ua](ua.hlean) : the univalence axiom +* [funext_varieties](funext_varieties.hlean) : versions of function extensionality +* [funext_of_ua](funext_of_ua.hlean) : univalence implies funext diff --git a/hott/init/init.md b/hott/init/init.md new file mode 100644 index 0000000000..1956fc274e --- /dev/null +++ b/hott/init/init.md @@ -0,0 +1,41 @@ +init +==== + +The modules in this folder are required by low-level operations, and +are always imported by default. You can suppress this behavior by +beginning a file with the keyword "prelude". + +Syntax declarations: + +* [reserved_notation](reserved_notation.hlean) +* [tactic](tactic.hlean) +* [priority](priority.hlean) + +Datatypes and logic: + +* [datatypes](datatypes.hlean) +* [logic](logic.hlean) +* [bool](bool.hlean) +* [num](num.hlean) +* [nat](nat.hlean) +* [function](function.hlean) +* [types](types/types.md) (subfolder) + +HoTT basics: + +* [path](path.hlean) +* [hedberg](hedberg.hlean) +* [trunc](trunc.hlean) +* [equiv](equiv.hlean) +* [axioms](axioms/axioms.md) (subfolder) + +Support for well-founded recursion and automation: + +* [relation](relation.hlean) +* [wf](wf.hlean) +* [util](util.hlean) + +The default import: + +* [default](default.hlean) + diff --git a/hott/init/types/types.md b/hott/init/types/types.md new file mode 100644 index 0000000000..019ef23c9c --- /dev/null +++ b/hott/init/types/types.md @@ -0,0 +1,9 @@ +init.types +========== + +Some basic datatypes. + +* [empty](empty.hlean) +* [prod](prod.hlean) +* [sigma](sigma.hlean) +* [sum](sum.hlean) \ No newline at end of file diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index 4f66bf8d62..85a33b36aa 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -2,7 +2,7 @@ Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Module: types.path +Module: types.eq Author: Floris van Doorn Ported from Coq HoTT diff --git a/hott/types/types.md b/hott/types/types.md new file mode 100644 index 0000000000..8fa5fbaa94 --- /dev/null +++ b/hott/types/types.md @@ -0,0 +1,15 @@ +hott.types +========== + +Various datatypes. + +* [pi](pi.hlean) +* [arrow](arrow.hlean) +* [eq](eq.hlean) +* [trunc](trunc.hlean) +* [prod](prod.hlean) +* [sigma](sigma.hlean) +* [fiber](fiber.hlean) +* [equiv](equiv.hlean) +* [pointed](pointed.hlean) +* [W](W.hlean) \ No newline at end of file diff --git a/library/algebra/algebra.md b/library/algebra/algebra.md index 10479cc7ab..ecc78ff069 100644 --- a/library/algebra/algebra.md +++ b/library/algebra/algebra.md @@ -11,5 +11,6 @@ Algebraic structures. * [ring](ring.lean) * [ordered_group](ordered_group.lean) * [ordered_ring](ordered_ring.lean) +* [field](field.lean) * [category](category/category.md) : category theory diff --git a/library/algebra/category/category.md b/library/algebra/category/category.md index 1699906018..ce646a70e4 100644 --- a/library/algebra/category/category.md +++ b/library/algebra/category/category.md @@ -1,5 +1,5 @@ -category -======= +algebra.category +================ Algebraic structures. diff --git a/library/library.md b/library/library.md index 7887f6e92f..2f27024c58 100644 --- a/library/library.md +++ b/library/library.md @@ -1,7 +1,7 @@ -The Lean Library -================ +The Lean Standard Library +========================= -The Lean library is contained in the following modules and directories: +The Lean standard library is contained in the following modules and directories: * [init](init/init.md) : constants and theorems needed for low-level system operations * [logic](logic/logic.md) : logical constructs and axioms @@ -29,5 +29,5 @@ lists, and so on. The `classical` library imports the law of the excluded middle, choice functions, and propositional extensionality. See `logic/axioms` for details. -See also the `hott` library, a library for homotopy type theory based on a predicative -foundation. +See also the [hott library](../hott/hott.md), a library for homotopy +type theory based on a predicative foundation.