From a567ef364e393caa500c17c146a2004efc21ad52 Mon Sep 17 00:00:00 2001
From: Dmitriy Gorshenin <dmitriy.gorshenin@gmail.com>
Date: Thu, 2 Jun 2022 19:39:03 +0300
Subject: [PATCH] =?UTF-8?q?=D0=A3=D0=B4=D0=B0=D0=BB=D0=B5=D0=BD=D0=B8?=
 =?UTF-8?q?=D0=B5=20=D1=84=D0=B0=D0=B9=D0=BB=D0=B0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 KompFunc | 8 --------
 1 file changed, 8 deletions(-)
 delete mode 100644 KompFunc

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).