diff --git a/homotopy/clive.hlean b/homotopy/clive.hlean
new file mode 100644
index 0000000..94b982e
--- /dev/null
+++ b/homotopy/clive.hlean
@@ -0,0 +1,9 @@
+import types.trunc types.arrow_2 types.fiber homotopy.susp homotopy.circle
+
+open eq is_trunc is_equiv nat equiv trunc function fiber circle
+
+namespace clive
+
+check 
+
+end clive