Lean4
/-- For a list, foldl f x [y₀,y₁] reduces as follows:
```
calc foldl f x [y₀,y₁]
= foldl f (f x y₀) [y₁] : rfl
... = foldl f (f (f x y₀) y₁) [] : rfl
... = f (f x y₀) y₁ : rfl
```
with
```
f : α → β → α
x : α
[y₀,y₁] : List β
```
We can view the above as a composition of functions:
```
... = f (f x y₀) y₁ : rfl
... = flip f y₁ (flip f y₀ x) : rfl
... = (flip f y₁ ∘ flip f y₀) x : rfl
```
We can use traverse and const to construct this composition:
```
calc const.run (traverse (fun y ↦ const.mk' (flip f y)) [y₀,y₁]) x
= const.run ((::) <$> const.mk' (flip f y₀) <*>
traverse (fun y ↦ const.mk' (flip f y)) [y₁]) x
... = const.run ((::) <$> const.mk' (flip f y₀) <*>
( (::) <$> const.mk' (flip f y₁) <*> traverse (fun y ↦ const.mk' (flip f y)) [] )) x
... = const.run ((::) <$> const.mk' (flip f y₀) <*>
( (::) <$> const.mk' (flip f y₁) <*> pure [] )) x
... = const.run ( ((::) <$> const.mk' (flip f y₁) <*> pure []) ∘
((::) <$> const.mk' (flip f y₀)) ) x
... = const.run ( const.mk' (flip f y₁) ∘ const.mk' (flip f y₀) ) x
... = const.run ( flip f y₁ ∘ flip f y₀ ) x
... = f (f x y₀) y₁
```
And this is how `const` turns a monoid into an applicative functor and
how the monoid of endofunctions define `Foldl`.
-/
abbrev Foldl (α : Type u) : Type u :=
(End α)ᵐᵒᵖ
