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

feat(hott.core): add more files to core.hlean

Browse source
This commit is contained in:
Floris van Doorn 2015-05-15 17:36:16 -04:00 committed by Leonardo de Moura
parent 2144036cdb
commit de6294a4ce
2 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/core.hlean
View file

@ -9,3 +9,5 @@ The core of the HoTT library
-/ -/
import types import types
import cubical.pathover cubical.square
import hit.circle

1
hott/types/default.hlean
View file

@ -7,3 +7,4 @@ Authors: Floris van Doorn
-/ -/
import .sigma .prod .pi .equiv .fiber .eq .trunc .arrow .pointed .function .trunc .bool import .sigma .prod .pi .equiv .fiber .eq .trunc .arrow .pointed .function .trunc .bool
import .nat .int