refactor(types): create cubical subfolder, update markdown files

hott/cubical/cubical.md

@@ -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

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

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:

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

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)

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

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₂)

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
 

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 .bool .prod .sigma .pi .arrow .pointed .fiber
-import .eq .square
+import .nat .int .cubical
-import .nat .int
+import .eq .equiv .function .trunc

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
 

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,
+      apply is_hprop.mk, intros,
-      fapply sigma_eq, {apply x.2},
+      fapply sigma_eq, apply x.2,
-      apply (@is_hprop.elimo)},
+      apply is_hprop.elimo},
     { intro A,
       apply is_trunc_is_equiv_closed,
       apply equiv.to_is_equiv,

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
 

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)

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