From 06528c4791d8d8b896e550e98b14957a38d37284 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 4 Jun 2015 13:55:02 -0400
Subject: [PATCH] refactor(types): create cubical subfolder, update markdown
 files

---
 hott/cubical/cubical.md                   |  9 ------
 hott/hit/interval.hlean                   |  2 +-
 hott/hott.md                              |  1 -
 hott/types/cubical/basic.hlean            | 36 +++++++++++++++++++++++
 hott/types/{ => cubical}/cube.hlean       |  0
 hott/types/{ => cubical}/cubeover.hlean   |  0
 hott/types/cubical/cubical.md             | 17 +++++++++++
 hott/types/cubical/default.hlean          |  8 +++++
 hott/types/{ => cubical}/pathover.hlean   | 12 +-------
 hott/types/{ => cubical}/square.hlean     |  0
 hott/types/{ => cubical}/squareover.hlean |  2 +-
 hott/types/default.hlean                  |  6 ++--
 hott/types/eq.hlean                       |  2 +-
 hott/types/hprop_trunc.hlean              |  6 ++--
 hott/types/trunc.hlean                    |  2 +-
 hott/types/types.md                       | 27 +++++++++--------
 hott/types/unit.hlean                     |  2 +-
 17 files changed, 88 insertions(+), 44 deletions(-)
 delete mode 100644 hott/cubical/cubical.md
 create mode 100644 hott/types/cubical/basic.hlean
 rename hott/types/{ => cubical}/cube.hlean (100%)
 rename hott/types/{ => cubical}/cubeover.hlean (100%)
 create mode 100644 hott/types/cubical/cubical.md
 create mode 100644 hott/types/cubical/default.hlean
 rename hott/types/{ => cubical}/pathover.hlean (92%)
 rename hott/types/{ => cubical}/square.hlean (100%)
 rename hott/types/{ => cubical}/squareover.hlean (99%)

diff --git a/hott/cubical/cubical.md b/hott/cubical/cubical.md
deleted file mode 100644
index d708d3c95..000000000
--- a/hott/cubical/cubical.md
+++ /dev/null
@@ -1,9 +0,0 @@
-hott.cubical
-============
-
-Implementation of Dan Licata's paper about [cubical ideas in HoTT](http://homotopytypetheory.org/2015/01/20/ts1s1-cubically/)
-
-* [pathover](pathover.hlean)
-* [square](square.hlean)
-
-TODO: squareover/cube/cubeover
\ No newline at end of file
diff --git a/hott/hit/interval.hlean b/hott/hit/interval.hlean
index 3aea6bb6d..9fee3b4a7 100644
--- a/hott/hit/interval.hlean
+++ b/hott/hit/interval.hlean
@@ -6,7 +6,7 @@ Authors: Floris van Doorn
 Declaration of the interval
 -/
 
-import .suspension types.eq types.prod types.square
+import .suspension types.eq types.prod types.cubical.square
 open eq suspension unit equiv equiv.ops is_trunc nat prod
 
 definition interval : Type₀ := suspension unit
diff --git a/hott/hott.md b/hott/hott.md
index 0076f1729..dac94008a 100644
--- a/hott/hott.md
+++ b/hott/hott.md
@@ -8,7 +8,6 @@ files and directories:
 * [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) : implementation of ideas from cubical type theory
 * [arity](arity.hlean) : a file containing theorems about functions with arity 2 or higher
 
 Lean's homotopy type theory kernel is a version of Martin-Löf Type Theory with:
diff --git a/hott/types/cubical/basic.hlean b/hott/types/cubical/basic.hlean
new file mode 100644
index 000000000..748ef827c
--- /dev/null
+++ b/hott/types/cubical/basic.hlean
@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Floris van Doorn
+
+Definition of squares, cubes, squareovers and cubeovers
+-/
+
+--path (eq) and pathover are defined in init.datatypes and init.pathover, respectively
+
+exit
+
+namespace eq
+
+  variable {A : Type}
+
+  inductive square {A : Type} {a₀₀ : A}
+    : Π{a₂₀ a₀₂ a₂₂ : A}, a₀₀ = a₂₀ → a₀₂ = a₂₂ → a₀₀ = a₀₂ → a₂₀ = a₂₂ → Type :=
+  ids : square idp idp idp idp
+
+  definition ids      [reducible] [constructor]         := @square.ids
+  definition idsquare [reducible] [constructor] (a : A) := @square.ids A a
+
+  inductive squareover {A : Type} (B : A → Type) {a₀₀ : A} {b₀₀ : B a₀₀} :
+    Π{a₂₀ a₀₂ a₂₂ : A}
+     {p₁₀ : a₀₀ = a₂₀} {p₁₂ : a₀₂ = a₂₂} {p₀₁ : a₀₀ = a₀₂} {p₂₁ : a₂₀ = a₂₂}
+     (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
+     {b₂₀ : B a₂₀} {b₀₂ : B a₀₂} {b₂₂ : B a₂₂}
+     (q₁₀ : pathover B b₀₀ p₁₀ b₂₀) (q₁₂ : pathover B b₀₂ p₁₂ b₂₂)
+     (q₀₁ : pathover B b₀₀ p₀₁ b₀₂) (q₂₁ : pathover B b₂₀ p₂₁ b₂₂),
+     Type :=
+  idsquareo : squareover B ids idpo idpo idpo idpo
+
+
+
+end eq
diff --git a/hott/types/cube.hlean b/hott/types/cubical/cube.hlean
similarity index 100%
rename from hott/types/cube.hlean
rename to hott/types/cubical/cube.hlean
diff --git a/hott/types/cubeover.hlean b/hott/types/cubical/cubeover.hlean
similarity index 100%
rename from hott/types/cubeover.hlean
rename to hott/types/cubical/cubeover.hlean
diff --git a/hott/types/cubical/cubical.md b/hott/types/cubical/cubical.md
new file mode 100644
index 000000000..5633661bd
--- /dev/null
+++ b/hott/types/cubical/cubical.md
@@ -0,0 +1,17 @@
+types.cubical
+=============
+
+Cubical Types:
+
+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
+* [squareover](squareover.hlean): square over a square
+* [cubeover](cubeover.hlean): cube over a cube
+
+Characterizing equality/pathovers in cubical types
+
+For [eq](../eq.hlean) this is done in the [types/](../types.md) folder
+
+* [pathover](pathover.hlean)
\ No newline at end of file
diff --git a/hott/types/cubical/default.hlean b/hott/types/cubical/default.hlean
new file mode 100644
index 000000000..2141b17f7
--- /dev/null
+++ b/hott/types/cubical/default.hlean
@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+
+import .square .cube .squareover .cubeover
+import .pathover
diff --git a/hott/types/pathover.hlean b/hott/types/cubical/pathover.hlean
similarity index 92%
rename from hott/types/pathover.hlean
rename to hott/types/cubical/pathover.hlean
index 833ac67e6..6789d904f 100644
--- a/hott/types/pathover.hlean
+++ b/hott/types/cubical/pathover.hlean
@@ -7,7 +7,7 @@ Pathovers.
 Note that the basic definitions are in init.pathover
 -/
 
-import types.squareover
+import .squareover
 
 open eq equiv is_equiv equiv.ops
 
@@ -19,16 +19,6 @@ namespace eq
             {c : C a b} {c₂ : C a₂ b₂}
             {q q' : a =[p] a₂}
 
-
---check λa, pathover (C a) (fc a) (h a) (gc a)
-
--- λa, pathover P (b a) (p a) (b' a)
-
-
-
--- pathover P b p b'
---set_option pp.notation false
-
   --in this version A' does not depend on A
   definition pathover_pathover_fl {a' a₂' : A'} {p : a' = a₂'} {a₂ : A} {f : A' → A}
     {b : Πa, B (f a)} {b₂ : B a₂} {q : Π(a' : A'), f a' = a₂} (r : pathover B (b a') (q a') b₂)
diff --git a/hott/types/square.hlean b/hott/types/cubical/square.hlean
similarity index 100%
rename from hott/types/square.hlean
rename to hott/types/cubical/square.hlean
diff --git a/hott/types/squareover.hlean b/hott/types/cubical/squareover.hlean
similarity index 99%
rename from hott/types/squareover.hlean
rename to hott/types/cubical/squareover.hlean
index 78626491f..e05bd128a 100644
--- a/hott/types/squareover.hlean
+++ b/hott/types/cubical/squareover.hlean
@@ -6,7 +6,7 @@ Author: Floris van Doorn
 Squareovers
 -/
 
-import types.square
+import .square
 
 open eq equiv is_equiv equiv.ops
 
diff --git a/hott/types/default.hlean b/hott/types/default.hlean
index d561eef83..1465d3c79 100644
--- a/hott/types/default.hlean
+++ b/hott/types/default.hlean
@@ -4,6 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 
-import .sigma .prod .pi .equiv .fiber .trunc .arrow .pointed .function .trunc .bool
-import .eq .square
-import .nat .int
+import .bool .prod .sigma .pi .arrow .pointed .fiber
+import .nat .int .cubical
+import .eq .equiv .function .trunc
diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean
index e859fcfac..9e8148d4a 100644
--- a/hott/types/eq.hlean
+++ b/hott/types/eq.hlean
@@ -7,7 +7,7 @@ Partially ported from Coq HoTT
 Theorems about path types (identity types)
 -/
 
-import .square
+import .cubical.square
 
 open eq sigma sigma.ops equiv is_equiv equiv.ops
 
diff --git a/hott/types/hprop_trunc.hlean b/hott/types/hprop_trunc.hlean
index 5c852225a..a1e60dd53 100644
--- a/hott/types/hprop_trunc.hlean
+++ b/hott/types/hprop_trunc.hlean
@@ -42,9 +42,9 @@ namespace is_trunc
     { intro A,
       apply is_trunc_is_equiv_closed,
       { apply equiv.to_is_equiv, apply is_contr.sigma_char},
-      apply (@is_hprop.mk), intros,
-      fapply sigma_eq, {apply x.2},
-      apply (@is_hprop.elimo)},
+      apply is_hprop.mk, intros,
+      fapply sigma_eq, apply x.2,
+      apply is_hprop.elimo},
     { intro A,
       apply is_trunc_is_equiv_closed,
       apply equiv.to_is_equiv,
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index b44370e60..021a4cffc 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -6,7 +6,7 @@ Authors: Floris van Doorn
 Properties of is_trunc and trunctype
 -/
 
---NOTE: the fact that (is_trunc n A) is a mere proposition is proved in .hprop_trunc
+-- 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
 
diff --git a/hott/types/types.md b/hott/types/types.md
index 9df8c5944..46f78a09e 100644
--- a/hott/types/types.md
+++ b/hott/types/types.md
@@ -1,24 +1,27 @@
 hott.types
 ==========
 
-Various datatypes.
+Types (not necessarily HoTT-related):
 
+* [unit](unit.hlean)
 * [bool](bool.hlean)
+* [nat](nat/nat.md) (subfolder)
+* [int](int/int.md) (subfolder)
 * [prod](prod.hlean)
 * [sigma](sigma.hlean)
 * [pi](pi.hlean)
 * [arrow](arrow.hlean)
-* [eq](eq.hlean)
-* [square](square.hlean): type of squares in a type
-* [fiber](fiber.hlean)
-* [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.
-* [equiv](equiv.hlean)
-* [pointed](pointed.hlean)
-* [function](function.hlean): embeddings, (split) surjections, retractions
-* [trunc](trunc.hlean): truncation levels, n-Types, truncation
 * [W](W.hlean): W-types (not loaded by default)
 
-Subfolders:
+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)
+* [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)
+
 
-* [nat](nat/nat.md)
-* [int](int/int.md)
\ No newline at end of file
diff --git a/hott/types/unit.hlean b/hott/types/unit.hlean
index 11b14b193..b77ac5be8 100644
--- a/hott/types/unit.hlean
+++ b/hott/types/unit.hlean
@@ -3,7 +3,7 @@ Copyright (c) 2015 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 
-Theorems about the booleans
+Theorems about the unit type
 -/
 
 open equiv option