From 9f13527c253e0939432d5004fb3e12e9ca72e541 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Fri, 13 May 2016 15:17:50 -0400
Subject: [PATCH] chore(hott): update default files and some markdown files

---
 hott/algebra/category/constructions/default.hlean | 2 +-
 hott/algebra/category/default.hlean               | 2 +-
 hott/algebra/category/functor/default.hlean       | 2 +-
 hott/algebra/category/limits/default.hlean        | 2 +-
 hott/core.hlean                                   | 5 +----
 hott/hit/default.hlean                            | 8 ++++++++
 hott/homotopy/cellcomplex.hlean                   | 8 --------
 hott/homotopy/default.hlean                       | 8 ++++++++
 hott/hott.md                                      | 9 +++++----
 hott/init/nat.hlean                               | 4 ++++
 hott/types/default.hlean                          | 2 +-
 hott/types/types.md                               | 3 ++-
 12 files changed, 33 insertions(+), 22 deletions(-)
 create mode 100644 hott/hit/default.hlean
 create mode 100644 hott/homotopy/default.hlean

diff --git a/hott/algebra/category/constructions/default.hlean b/hott/algebra/category/constructions/default.hlean
index c8d65bd74..a21161579 100644
--- a/hott/algebra/category/constructions/default.hlean
+++ b/hott/algebra/category/constructions/default.hlean
@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 
-import .functor .set .opposite .product .comma .sum .discrete .indiscrete .terminal .initial
+import .functor .set .opposite .product .comma .sum .discrete .indiscrete .terminal .initial .order
diff --git a/hott/algebra/category/default.hlean b/hott/algebra/category/default.hlean
index 6fdf85f8c..f6fe52068 100644
--- a/hott/algebra/category/default.hlean
+++ b/hott/algebra/category/default.hlean
@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 
-import .category .strict .groupoid .constructions
+import .category .strict .groupoid .constructions .limits .functor
diff --git a/hott/algebra/category/functor/default.hlean b/hott/algebra/category/functor/default.hlean
index 8274c00c1..3eb119451 100644
--- a/hott/algebra/category/functor/default.hlean
+++ b/hott/algebra/category/functor/default.hlean
@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 
-import .basic
+import .exponential_laws
diff --git a/hott/algebra/category/limits/default.hlean b/hott/algebra/category/limits/default.hlean
index e936fa68f..adb88e42c 100644
--- a/hott/algebra/category/limits/default.hlean
+++ b/hott/algebra/category/limits/default.hlean
@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 
-import .limits .colimits
+import .set .functor .adjoint .functor_preserve
diff --git a/hott/core.hlean b/hott/core.hlean
index 0c35225df..063223bf3 100644
--- a/hott/core.hlean
+++ b/hott/core.hlean
@@ -6,7 +6,4 @@ Authors: Floris van Doorn
 The core of the HoTT library
 -/
 
-import types
-import cubical
-import homotopy.circle
-import algebra.hott
+import types cubical homotopy hit choice
diff --git a/hott/hit/default.hlean b/hott/hit/default.hlean
new file mode 100644
index 000000000..2ddfc9354
--- /dev/null
+++ b/hott/hit/default.hlean
@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2016 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+
+-/
+
+import .two_quotient .colimit .coeq .refl_quotient
diff --git a/hott/homotopy/cellcomplex.hlean b/hott/homotopy/cellcomplex.hlean
index ad21d442b..cd7f8771f 100644
--- a/hott/homotopy/cellcomplex.hlean
+++ b/hott/homotopy/cellcomplex.hlean
@@ -10,14 +10,6 @@ open eq is_trunc is_equiv nat equiv trunc prod pushout sigma sphere_index unit
 -- where should this be?
 definition family : Type := ΣX, X → Type
 
--- this should be in init!
-namespace nat
-
-  definition cases {M : ℕ → Type} (mz : M zero) (ms : Πn, M (succ n)) : Πn, M n :=
-  nat.rec mz (λn dummy, ms n)
-
-end nat
-
 namespace cellcomplex
 
   /-
diff --git a/hott/homotopy/default.hlean b/hott/homotopy/default.hlean
new file mode 100644
index 000000000..6048262cf
--- /dev/null
+++ b/hott/homotopy/default.hlean
@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2016 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+
+-/
+
+import .sphere2 .EM .torus .red_susp .quaternionic_hopf .smash .cellcomplex .interval .cylinder
diff --git a/hott/hott.md b/hott/hott.md
index 4df47054c..748701e06 100644
--- a/hott/hott.md
+++ b/hott/hott.md
@@ -3,11 +3,12 @@ The Lean Homotopy Type Theory Library
 
 The Lean Homotopy Type Theory library consists of the following directories:
 
-* [init](init/init.md) : constants and theorems needed for low-level system operations
+* [init](init/init.md) : basic definitions and theorems. These are imported in each ".hlean" file by default, unless the `prelude` command is used.
 * [types](types/types.md) : concrete datatypes and type constructors
-* [hit](hit/hit.md): higher inductive types
-* [algebra](algebra/algebra.md) : algebraic structures
-* [cubical](cubical/cubical.md): cubical types
+* [algebra](algebra/algebra.md) : algebraic structures, group theory and category theory.
+* [cubical](cubical/cubical.md) : cubical types (e.g. squares in a types, squareovers)
+* [hit](hit/hit.md): higher inductive types. Some higher inductive types which are mostly relevant in homotopy theory are in the [homotopy](homotopy/homotopy.md) folder.
+* [homotopy](homotopy/homotopy.md) : synthetic homotopy theory.
 
 The following files don't fit in any of the subfolders:
 * [prop_trunc](prop_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.
diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean
index 92bc54632..be8aff41a 100644
--- a/hott/init/nat.hlean
+++ b/hott/init/nat.hlean
@@ -16,6 +16,10 @@ namespace nat
                        {C : ℕ → Type} (n : ℕ) (H₁ : C 0) (H₂ : Π (a : ℕ), C a → C (succ a)) : C n :=
   nat.rec H₁ H₂ n
 
+  protected definition cases [reducible] [unfold 4] {M : ℕ → Type} (mz : M zero)
+    (ms : Πn, M (succ n)) : Πn, M n :=
+  nat.rec mz (λn dummy, ms n)
+
   protected definition cases_on [reducible] [recursor] [unfold 2]
                        {C : ℕ → Type} (n : ℕ) (H₁ : C 0) (H₂ : Π (a : ℕ), C (succ a)) : C n :=
   nat.rec H₁ (λ a ih, H₂ a) n
diff --git a/hott/types/default.hlean b/hott/types/default.hlean
index 1f2f9b7ae..2ba8f0212 100644
--- a/hott/types/default.hlean
+++ b/hott/types/default.hlean
@@ -6,4 +6,4 @@ Authors: Floris van Doorn
 
 import .bool .unit .prod .sigma .pi .arrow .pointed .fiber
 import .nat .int
-import .eq .equiv .trunc
+import .eq .equiv .trunc .univ .W .type_functor
diff --git a/hott/types/types.md b/hott/types/types.md
index 0efe5ec31..4da764298 100644
--- a/hott/types/types.md
+++ b/hott/types/types.md
@@ -29,4 +29,5 @@ Types in HoTT:
 * [equiv](equiv.hlean)
 * [trunc](trunc.hlean): truncation levels, n-types, truncation
 * [pullback](pullback.hlean)
-* [univ](univ.hlean)
\ No newline at end of file
+* [univ](univ.hlean)
+* [type_functor](type_functor.hlean)
\ No newline at end of file