From 5342e4186393e49ee96ff32757830f86e40b631c Mon Sep 17 00:00:00 2001
From: cnewstead <cnewstead@cmu.edu>
Date: Thu, 18 Feb 2016 14:04:05 -0500
Subject: [PATCH] Delete clive.hlean

---
 homotopy/clive.hlean | 42 ------------------------------------------
 1 file changed, 42 deletions(-)
 delete mode 100644 homotopy/clive.hlean

diff --git a/homotopy/clive.hlean b/homotopy/clive.hlean
deleted file mode 100644
index a602661..0000000
--- a/homotopy/clive.hlean
+++ /dev/null
@@ -1,42 +0,0 @@
-/-----
-This is Clive's file for playing around with (h)Lean/Git/Emacs
-------/
-
-import types.trunc types.arrow_2 types.fiber homotopy.circle
-
-open eq is_trunc is_equiv nat equiv trunc function circle
-
-
-
-namespace clive
-
-/-- Very easy goal: prove (loop⁻¹)⁻¹ = loop : base = base --/
-theorem symm_symm_loop_eq_loop : (loop⁻¹)⁻¹ = loop :=
-eq.rec_on loop idp
-
-/-- Another easy goal: define a group and prove that the left inverse law follows form the right inverse law --/
-structure group (X : Type) :=
-gpstr :: (unit      : X)
-         (mult       : X → X → X)
-         (inv       : X → X)
-         (assoc_law : Π(a b c : X), mult (mult a b) c = mult a (mult b c))
-         (inv_law   : Π(a : X), mult a (inv a) = unit)
-         (unit_law  : Π(a : X), mult a unit = a)
-
-constants (X : Type) (G : group X)
-open group
-
-theorem group_cancel_right : Π(X : Type), Π(G : group X), Π(a b c : X), (mult G a c = mult G b c) → a = b := sorry
-
-theorem inv_mul_left_eq_unit : Π(X : Type), Π(G : group X), Π(a : X), mult G (inv G a) a = unit G :=
-  take (X : Type) (G : group X) (a : X),
-  have q : mult G (mult G (inv G a) a) (inv G a) = mult G (unit G) (inv G a), from
-  calc
-    mult G (mult G (inv G a) a) (inv G a) = mult G (inv G a) (mult G a (inv G a)) : assoc_law
-    ... = mult G (inv G a) (unit G) : sorry
-    ... = inv G a : unit_law
-    ... = mult G  (unit G) (inv G a) : sorry,
-  group_cancel_right X G (mult G (inv G a) a) (unit G) (inv G a) q
-
-
-end clive