diff --git a/KompFunc b/KompFunc
deleted file mode 100644
index d245101..0000000
--- a/KompFunc
+++ /dev/null
@@ -1,8 +0,0 @@
- Definition cf := fun t0 t1 t2 : Type
-   => fun (f : t1 -> t2) (g : t0 -> t1) => fun x => f (g x).
- Implicit Arguments cf [t0 t1 t2].
- Notation "f @ g" := (cf f g) (at level 65, left associativity).
- 
- Definition cf_assoc := fun (t0 t1 t2 t3 : Type)
-   (f : t2 -> t3) (g : t1 -> t2) (h : t0 -> t1)
-   => (refl_equal _) : (f @ g) @ h = f @ (g @ h).