Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-05 09:56 a64be8dc

View on Github →

feat(category/bifunctor): Bifunctor and bitraversable (#255)

Estimated changes

Modified category/applicative.lean

Created category/bifunctor.lean

added def bifunctor.bicompl

added def bifunctor.bicompr

added theorem bifunctor.comp_fst

added theorem bifunctor.comp_snd

added def bifunctor.fst

added theorem bifunctor.fst_snd

added theorem bifunctor.id_fst

added theorem bifunctor.id_snd

added def bifunctor.snd

added theorem bifunctor.snd_fst

Created category/bitraversable/basic.lean

added def bisequence

Created category/bitraversable/instances.lean

added def bicompl.bitraverse

added def bicompr.bitraverse

added def const.bitraverse

added def flip.bitraverse

added def prod.bitraverse

added def sum.bitraverse

Created category/bitraversable/lemmas.lean

added theorem bitraversable.comp_tfst

added theorem bitraversable.comp_tsnd

added theorem bitraversable.id_tfst

added theorem bitraversable.id_tsnd

added def bitraversable.tfst

added theorem bitraversable.tfst_eq_fst_id

added theorem bitraversable.tfst_tsnd

added def bitraversable.tsnd

added theorem bitraversable.tsnd_eq_snd_id

added theorem bitraversable.tsnd_tfst

Modified category/functor.lean

added def functor.add_const

added def functor.const.mk

added def functor.const.run

added def functor.const

Modified category/traversable/instances.lean

Modified data/sum.lean

deleted def sum.map

Modified tactic/basic.lean