diff --git a/hott/algebra/category/functor/curry.hlean b/hott/algebra/category/functor/curry.hlean
deleted file mode 100644
index 9ada0b4ca..000000000
--- a/hott/algebra/category/functor/curry.hlean
+++ /dev/null
@@ -1,7 +0,0 @@
-/-
-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
-
-Definition of currying and uncurrying of functors
--/