commit 3e5775b4ef6da0c4fe7462dde8482acf9d52e4cf
Author: Dmitriy Gorshenin <dmitriy.gorshenin@gmail.com>
Date:   Tue May 31 22:43:41 2022 +0300

    Ассоциативность композиции функций

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