Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-16 12:59 844c665b

View on Github →

feat(category/applicative): id and comp functors; proofs by norm (#184)

Estimated changes

added theorem comp.map_pure
added theorem comp.pure_seq_eq_map
added theorem comp.seq_assoc
added theorem comp.seq_mk
added theorem comp.seq_pure
deleted theorem map_map
deleted def mmap₂
added def mzip_with'
added def mzip_with
added theorem functor.comp.map_mk
added structure functor.comp
added theorem functor.map_comp_map
added theorem functor.map_id
added def id.mk