michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(hott): add core.hlean and types/default.hlean

Browse source
This commit is contained in:
Floris van Doorn 2015-04-09 22:14:19 -04:00 committed by Leonardo de Moura
parent d1b98b6919
commit 60ae9f627c
4 changed files with 25 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
hott/core.hlean Normal file
View file

@ -0,0 +1,11 @@
/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: core
Authors: Floris van Doorn
The core of the HoTT library
-/
import types

2
hott/hott.md
View file

@ -14,6 +14,8 @@ Lean's homotopy type theory kernel is a version of Martin-Löf Type Theory with:
* a non-cumulative hierarchy of universes, `Type 0`, `Type 1`, ... * a non-cumulative hierarchy of universes, `Type 0`, `Type 1`, ...
* inductively defined types * inductively defined types
Note that there is no proof-irrelevant or impredicative universe.
By default, the univalence axiom is declared on initialization. By default, the univalence axiom is declared on initialization.
See also the [standard library](../library/library.md). See also the [standard library](../library/library.md).

11
hott/types/default.hlean Normal file
View file

@ -0,0 +1,11 @@
/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: types.default
Authors: Floris van Doorn
The core of the HoTT library
-/
import .sigma .prod .pi .equiv .fiber .eq .trunc .arrow .pointed

2
hott/types/types.md
View file

@ -12,4 +12,4 @@ Various datatypes.
* [fiber](fiber.hlean) * [fiber](fiber.hlean)
* [equiv](equiv.hlean) * [equiv](equiv.hlean)
* [pointed](pointed.hlean) * [pointed](pointed.hlean)
* [W](W.hlean) * [W](W.hlean) (not loaded by default)