From 2fed4706b6df212f20bcd9dee98bd645aa006d1c Mon Sep 17 00:00:00 2001
From: Dmitriy Gorshenin <dmitriy.gorshenin@gmail.com>
Date: Thu, 2 Jun 2022 19:43:57 +0300
Subject: [PATCH] =?UTF-8?q?=D0=90=D1=81=D1=81=D0=BE=D1=86=D0=B8=D0=B0?=
 =?UTF-8?q?=D1=82=D0=B8=D0=B2=D0=BD=D0=BE=D1=81=D1=82=D1=8C=20=D0=BA=D0=BE?=
 =?UTF-8?q?=D0=BC=D0=BF=D0=BE=D0=B7=D0=B8=D1=86=D0=B8=D0=B8=20=D1=84=D1=83?=
 =?UTF-8?q?=D0=BD=D0=BA=D1=86=D0=B8=D0=B9?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 KompFunc.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 KompFunc.v

diff --git a/KompFunc.v b/KompFunc.v
new file mode 100644
index 0000000..d245101
--- /dev/null
+++ b/KompFunc.v
@@ -0,0 +1,8 @@
+ 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).