lean2/hott/init/init.md

init
====

The files 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)

Datatypes and logic:

* [logic](logic.hlean)
* [datatypes](datatypes.hlean) (declaration of common types)
* [bool](bool.hlean)
* [num](num.hlean)
* [nat](nat.hlean)
* [function](function.hlean)
* [types](types.hlean) (notation and some theorems for the remaining basic types)
* [connectives](connectives.hlean)

HoTT basics:

* [path](path.hlean)
* [pathover](pathover.hlean)
* [hedberg](hedberg.hlean)
* [trunc](trunc.hlean)
* [equiv](equiv.hlean)
* [pointed](pointed.hlean)
* [ua](ua.hlean) (declaration of the univalence axiom, and some basic properties)
* [funext](funext.hlean) (proof of equivalence of certain notions of function exensionality, and a proof that function extensionality follows from univalence)

Support for well-founded recursion and automation:

* [relation](relation.hlean)
* [wf](wf.hlean)
* [util](util.hlean)

The default import:

* [default](default.hlean)
feat(*.md): create markdown files for HoTT library, update ones in standard library 2015-03-05 02:06:39 +00:00			`init`
			`====`

fix(hott/.md,library/.md): use the word 'file' instead of 'module' 2015-05-24 08:36:26 +00:00			`The files in this folder are required by low-level operations, and`
feat(*.md): create markdown files for HoTT library, update ones in standard library 2015-03-05 02:06:39 +00:00			`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)`

			`Datatypes and logic:`

			`* [logic](logic.hlean)`
refactor(hott.init): remove subdirectories, merge some files 2015-04-24 23:58:50 +00:00			`* [datatypes](datatypes.hlean) (declaration of common types)`
feat(*.md): create markdown files for HoTT library, update ones in standard library 2015-03-05 02:06:39 +00:00			`* [bool](bool.hlean)`
			`* [num](num.hlean)`
			`* [nat](nat.hlean)`
			`* [function](function.hlean)`
refactor(hott.init): remove subdirectories, merge some files 2015-04-24 23:58:50 +00:00			`* [types](types.hlean) (notation and some theorems for the remaining basic types)`
fix(hott): add missing links to markdown files 2016-02-23 18:00:16 +00:00			`* [connectives](connectives.hlean)`
feat(*.md): create markdown files for HoTT library, update ones in standard library 2015-03-05 02:06:39 +00:00
			`HoTT basics:`

			`* [path](path.hlean)`
fix(hott): add missing links to markdown files 2016-02-23 18:00:16 +00:00			`* [pathover](pathover.hlean)`
feat(*.md): create markdown files for HoTT library, update ones in standard library 2015-03-05 02:06:39 +00:00			`* [hedberg](hedberg.hlean)`
			`* [trunc](trunc.hlean)`
			`* [equiv](equiv.hlean)`
feat(pointed): merge pointed2 into pointed We move the basic notions of pointed types into init.pointed, to avoid cycles in the import graph. Also adds pointed versions of pi and sigma, with corresponding notation 2016-03-28 20:33:33 +00:00			`* [pointed](pointed.hlean)`
refactor(hott.init): remove subdirectories, merge some files 2015-04-24 23:58:50 +00:00			`* [ua](ua.hlean) (declaration of the univalence axiom, and some basic properties)`
			`* [funext](funext.hlean) (proof of equivalence of certain notions of function exensionality, and a proof that function extensionality follows from univalence)`
feat(*.md): create markdown files for HoTT library, update ones in standard library 2015-03-05 02:06:39 +00:00
			`Support for well-founded recursion and automation:`

			`* [relation](relation.hlean)`
			`* [wf](wf.hlean)`
			`* [util](util.hlean)`

			`The default import:`

			`* [default](default.hlean)`