From f995e5ea48bd31f5f5c9ff2631e8e37935384cad Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 4 Jun 2015 20:21:52 -0400
Subject: [PATCH] fix(cubical): remove unused basic file

---
 hott/types/cubical/basic.hlean | 36 ----------------------------------
 1 file changed, 36 deletions(-)
 delete mode 100644 hott/types/cubical/basic.hlean

diff --git a/hott/types/cubical/basic.hlean b/hott/types/cubical/basic.hlean
deleted file mode 100644
index 748ef827c..000000000
--- a/hott/types/cubical/basic.hlean
+++ /dev/null
@@ -1,36 +0,0 @@
-/-
-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