Mathlib Changelog
Changelog
About
Github
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