refactor(hott): move cubical folder and files eq2, function and hprop_trunc from types/ to the root HoTT directory

hott/algebra/category/adjoint.hlean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 
-import algebra.category.constructions .constructions types.function arity
+import algebra.category.constructions .constructions function arity
 
 open category functor nat_trans eq is_trunc iso equiv prod trunc function
 

hott/algebra/e_closure.hlean

@@ -7,7 +7,7 @@ The "equivalence closure" of a type-valued relation.
 Given a binary type-valued relation (fibration), we add reflexivity, symmetry and transitivity terms
 -/
 
-import .relation types.eq2 arity
+import .relation eq2 arity
 
 open eq
 

hott/algebra/hott.hlean

@@ -6,7 +6,7 @@ Author: Floris van Doorn
 Theorems about algebra specific to HoTT
 -/
 
-import .group arity types.pi types.hprop_trunc
+import .group arity types.pi hprop_trunc
 
 open equiv eq equiv.ops is_trunc
 

hott/book.md

@@ -29,7 +29,7 @@ The rows indicate the chapters, the columns the sections.
 
 Things not in the book:
 
-* One major difference is that in this library we heavily use pathovers, so we need less theorems about transports, but instead corresponding theorems about pathovers. These are in [init.pathover](init/pathover.hlean). For higher paths there are [squares](types/cubical/square.hlean), [squareovers](types/cubical/squareover.hlean), and the rudiments of [cubes](types/cubical/cube.hlean) and [cubeovers](types/cubical/cubeover.hlean).
+* One major difference is that in this library we heavily use pathovers, so we need less theorems about transports, but instead corresponding theorems about pathovers. These are in [init.pathover](init/pathover.hlean). For higher paths there are [squares](cubical/square.hlean), [squareovers](cubical/squareover.hlean), and the rudiments of [cubes](cubical/cube.hlean) and [cubeovers](cubical/cubeover.hlean).
 
 Chapter 1: Type theory
 ---------
@@ -60,7 +60,7 @@ Chapter 2: Homotopy type theory
 - 2.8 (The unit type): special case of [init.trunc](init/trunc.hlean)
 - 2.9 (Π-types and the function extensionality axiom): [init.funext](init/funext.hlean) and [types.pi](types/pi.hlean)
 - 2.10 (Universes and the univalence axiom): [init.ua](init/ua.hlean)
-- 2.11 (Identity type): [init.equiv](init/equiv.hlean) (ap is equivalence), [types.eq](types/eq.hlean) and [types.cubical.square](types/cubical/square.hlean) (characterization of pathovers in equality types)
+- 2.11 (Identity type): [init.equiv](init/equiv.hlean) (ap is equivalence), [types.eq](types/eq.hlean) and [cubical.square](cubical/square.hlean) (characterization of pathovers in equality types)
 - 2.12 (Coproducts): [types.sum](types/sum.hlean)
 - 2.13 (Natural numbers): [types.nat.hott](types/nat/hott.hlean)
 - 2.14 (Example: equality of structures): algebra formalized in [algebra.group](algebra/group.hlean).
@@ -71,7 +71,7 @@ Chapter 3: Sets and logic
 
 - 3.1 (Sets and n-types): [init.trunc](init/trunc.hlean)
 - 3.2 (Propositions as types?): not formalized
-- 3.3 (Mere propositions): [init.trunc](init/trunc.hlean) and [types.hprop_trunc](types/hprop_trunc.hlean) (Lemma 3.3.5).
+- 3.3 (Mere propositions): [init.trunc](init/trunc.hlean) and [hprop_trunc](hprop_trunc.hlean) (Lemma 3.3.5).
 - 3.4 (Classical vs. intuitionistic logic): decidable is defined in [init.logic](init/logic.hlean)
 - 3.5 (Subsets and propositional resizing): Lemma 3.5.1 is subtype_eq in [types.sigma](types/sigma.hlean), we don't have propositional resizing as axiom yet.
 - 3.6 (The logic of mere propositions): in the corresponding file in the [types](types/types.md) folder. (is_trunc_prod is defined in [types.sigma](types/sigma.hlean))
@@ -89,7 +89,7 @@ Chapter 4: Equivalences
 - 4.3 (Bi-invertible maps): not formalized
 - 4.4 (Contractible fibers): [types.equiv](types/equiv.hlean)
 - 4.5 (On the definition of equivalences): no formalizable content
-- 4.6 (Surjections and embeddings): [types.function](types/function.hlean)
+- 4.6 (Surjections and embeddings): [function](function.hlean)
 - 4.7 (Closure properties of equivalences): not formalized
 - 4.8 (The object classifier): not formalized
 - 4.9 (Univalence implies function extensionality): [init.funext](init/funext.hlean)
@@ -126,7 +126,7 @@ Chapter 6: Higher inductive types
 Chapter 7: Homotopy n-types
 ---------
 
-- 7.1 (Definition of n-types): [init.trunc](init/trunc.hlean), [types.trunc](types/trunc.hlean), [types.sigma](types/sigma.hlean) (Theorem 7.1.8), [types.pi](types/pi.hlean) (Theorem 7.1.9), [types.hprop_trunc](types/hprop_trunc.hlean) (Theorem 7.1.10)
+- 7.1 (Definition of n-types): [init.trunc](init/trunc.hlean), [types.trunc](types/trunc.hlean), [types.sigma](types/sigma.hlean) (Theorem 7.1.8), [types.pi](types/pi.hlean) (Theorem 7.1.9), [hprop_trunc](hprop_trunc.hlean) (Theorem 7.1.10)
 - 7.2 (Uniqueness of identity proofs and Hedberg’s theorem): [init.hedberg](init/hedberg.hlean) and [types.trunc](types/trunc.hlean)
 - 7.3 (Truncations): [init.hit](init/hit.hlean), [hit.trunc](hit/trunc.hlean) and [types.trunc](types/trunc.hlean)
 - 7.4 (Colimits of n-types): not formalized

hott/core.hlean

@@ -7,5 +7,6 @@ The core of the HoTT library
 -/
 
 import types
+import cubical
 import hit.circle
 import algebra.hott

hott/cubical/cubical.md

@@ -3,7 +3,7 @@ types.cubical
 
 Cubical Types:
 
-The files [path](../../init/path.hlean) and [pathover](../../init/pathover.hlean) are in the [init/](../../init/init.md) folder.
+The files [path](../init/path.hlean) and [pathover](../init/pathover.hlean) are in the [init/](../init/init.md) folder.
 
 * [square](square.hlean): square in a type
 * [cube](cube.hlean): cube in a type

hott/function.hlean

@@ -7,7 +7,7 @@ Ported from Coq HoTT
 Theorems about embeddings and surjections
 -/
 
-import hit.trunc .pi .fiber .equiv
+import hit.trunc types.equiv
 
 open equiv sigma sigma.ops eq trunc is_trunc pi is_equiv fiber prod
 

hott/hit/interval.hlean

@@ -6,7 +6,7 @@ Authors: Floris van Doorn
 Declaration of the interval
 -/
 
-import .susp types.eq types.prod types.cubical.square
+import .susp types.eq types.prod cubical.square
 open eq susp unit equiv equiv.ops is_trunc nat prod
 
 definition interval : Type₀ := susp unit

hott/hit/refl_quotient.hlean

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

hott/hit/susp.hlean

@@ -6,7 +6,7 @@ Authors: Floris van Doorn
 Declaration of suspension
 -/
 
-import .pushout types.pointed types.cubical.square
+import .pushout types.pointed cubical.square
 
 open pushout unit eq equiv equiv.ops
 

hott/hit/two_quotient.hlean

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

hott/hott.md

@@ -1,14 +1,19 @@
 The Lean Homotopy Type Theory Library
 =====================================
 
-The Lean homotopy type theory library is contained in the following
+The Lean Homotopy Type Theory library consists of the following directories:
-files and directories:
 
 * [init](init/init.md) : constants and theorems needed for low-level system operations
 * [types](types/types.md) : concrete datatypes and type constructors
 * [hit](hit/hit.md): higher inductive types
 * [algebra](algebra/algebra.md) : algebraic structures
-* [arity](arity.hlean) : a file containing theorems about functions with arity 2 or higher
+* [cubical](cubical/cubical.md): cubical types
+
+The following files don't fit in any of the subfolders:
+* [hprop_trunc](hprop_trunc.hlean): in this file we prove that `is_trunc n A` is a mere proposition. We separate this from [types.trunc](types/trunc.hlean) to avoid circularity in imports.
+* [eq2](eq2.hlean): coherence rules for the higher dimensional structure of equality
+* [function](function.hlean): embeddings, (split) surjections, retractions
+* [arity](arity.hlean) : equality theorems about functions with arity 2 or higher
 
 See [book.md](book.md) for an overview of the sections of the [HoTT book](http://homotopytypetheory.org/book/) which have been covered.
 

hott/hprop_trunc.hlean

@@ -8,7 +8,7 @@ We prove this here to avoid circular dependency of files
 We want to use this in .equiv; .equiv is imported by .function and .function is imported by .trunc
 -/
 
-import .pi
+import types.pi
 
 open equiv sigma sigma.ops eq function pi
 

hott/types/default.hlean

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

hott/types/equiv.hlean

@@ -7,7 +7,7 @@ Ported from Coq HoTT
 Theorems about the types equiv and is_equiv
 -/
 
-import .fiber .arrow arity .hprop_trunc
+import .fiber .arrow arity ..hprop_trunc
 
 open eq is_trunc sigma sigma.ops pi fiber function equiv equiv.ops
 

hott/types/trunc.hlean

@@ -8,7 +8,7 @@ Properties of is_trunc and trunctype
 
 -- NOTE: the fact that (is_trunc n A) is a mere proposition is proved in .hprop_trunc
 
-import types.pi types.eq types.equiv .function
+import types.pi types.eq types.equiv ..function
 
 open eq sigma sigma.ops pi function equiv is_trunc.trunctype
      is_equiv prod is_trunc.trunc_index pointed nat

hott/types/types.md

@@ -16,14 +16,9 @@ Types (not necessarily HoTT-related):
 
 HoTT types
 
-* [hprop_trunc](hprop_trunc.hlean): in this file we prove that `is_trunc n A` is a mere proposition. We separate this from [trunc](trunc.hlean) to avoid circularity in imports.
 * [eq](eq.hlean): show that functions related to the identity type are equivalences
-* [eq2](eq2.hlean): higher dimensional structure of equality
 * [pointed](pointed.hlean)
 * [fiber](fiber.hlean)
 * [equiv](equiv.hlean)
-* [function](function.hlean): embeddings, (split) surjections, retractions
 * [trunc](trunc.hlean): truncation levels, n-Types, truncation
-* [cubical](cubical/cubical.md): cubical types (subfolder)
-