mathlib3

93cdc3a5 - feat(control/traversable/basic): composition of applicative transformations (#4487)

feat(control/traversable/basic): composition of applicative transformations (#4487) Added composition law for applicative transformations, added rest of interface for coercion of applicative transformations to functions (lifted from `monoid_hom`), and proved composition was associative and has an identity. Also corrected some documentation.