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

2022-05-31 22:43:41 +03:00
commit 3e5775b4ef
1 changed files with 8 additions and 0 deletions
--- a/8
+++ b/8
@@ -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).