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

fix(hott): import commands (some files have been moved to different directories)

Browse source
This commit is contained in:
Leonardo de Moura 2015-09-25 09:39:45 -07:00
parent 719e9043cd
commit 4a6ff8058d
4 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/core.hlean
View file

@ -8,5 +8,5 @@ The core of the HoTT library
import types
import cubical
import hit.circle
import homotopy.circle
import algebra.hott

2
hott/hit/refl_quotient.hlean
View file

@ -7,7 +7,7 @@ Authors: Floris van Doorn
Quotient of a reflexive relation
-/
import hit.circle cubical.squareover .two_quotient
import homotopy.circle cubical.squareover .two_quotient
open eq simple_two_quotient e_closure

2
hott/hit/two_quotient.hlean
View file

@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
-/
import hit.circle eq2 algebra.e_closure cubical.cube
import homotopy.circle eq2 algebra.e_closure cubical.cube
open quotient eq circle sum sigma equiv function relation

2
hott/homotopy/cellcomplex.hlean
View file

@ -3,7 +3,7 @@ Copyright (c) 2015 Ulrik Buchholtz. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Ulrik Buchholtz
-/
import types.trunc hit.sphere hit.pushout
import types.trunc homotopy.sphere hit.pushout
open eq is_trunc is_equiv nat equiv trunc prod pushout sigma sphere_index unit