Commit 2020-10-07 01:06 93cdc3a5

View on Github →

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.

Estimated changes

Modified src/control/traversable/basic.lean

added theorem applicative_transformation.app_eq_coe

added theorem applicative_transformation.coe_inj

added theorem applicative_transformation.coe_mk

added def applicative_transformation.comp

added theorem applicative_transformation.comp_apply

added theorem applicative_transformation.comp_assoc

added theorem applicative_transformation.comp_id

added theorem applicative_transformation.congr_arg

added theorem applicative_transformation.congr_fun

added theorem applicative_transformation.ext

added theorem applicative_transformation.ext_iff

added theorem applicative_transformation.id_comp

added theorem applicative_transformation.preserves_map'