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

fix(types.md): add num

Browse source
This commit is contained in:
Floris van Doorn 2015-12-09 00:17:42 -05:00 committed by Leonardo de Moura
parent f495fa04c8
commit 65c93b180d
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
hott/types/types.md
View file

@ -1,10 +1,11 @@
hott.types
==========
Types (not necessarily HoTT-related):
Types in Martin-Lӧf Type Theory:
* [unit](unit.hlean)
* [bool](bool.hlean)
* [num[(num.hlean) (natural numbers written in binary form)
* [nat](nat/nat.md) (subfolder)
* [int](int/int.md) (subfolder)
* [prod](prod.hlean)
@ -17,7 +18,9 @@ Types (not necessarily HoTT-related):
* [lift](lift.hlean)
* [list](list.hlean)
HoTT types
The number systems (num, nat, int, ...) are for a large part ported from the standard libary.
Specific HoTT types
* [eq](eq.hlean): show that functions related to the identity type are equivalences
* [pointed](pointed.hlean): pointed types, maps, homotopies, and equivalences