Structures · Data types
Bitraversable
Lawless bitraversable bifunctor. This only holds data for the bimap and bitraverse.
- Defined in
- Mathlib.Control.Bitraversable.Basic
- Shape
- One type argument · adds bitraverse
Extends1
Extended by0
Nothing extends this class yet.
Forgetful instances
Every Bitraversable is also a
Concrete types that are instances6
- Functor.Const
- flip
- Function.bicompl
- Function.bicompr
- Prod
- Sum
How is a type an instance?
Loading the hierarchy index…
Assumed by32
- Bitraversable.bitraverse
- Bitraversable.tsnd
- Bitraversable.tfst
- Bitraversable.tfst_eq_fst_id
- Bitraversable.tsnd_eq_snd_id
- Bitraversable.comp_tfst
- Bitraversable.tsnd_tfst
- Bitraversable.comp_tsnd
- Bitraversable.tfst_tsnd
- Bitraversable.id_tsnd
- Bitraversable.id_tfst
- Bitraversable.flip
- instBitraversableBicompl
- Bitraversable.tsnd_id
- Bitraversable.tsnd_comp_tsnd
- flip.bitraverse
- Bitraversable.tfst_id
- LawfulBitraversable.flip
- Bitraversable.toBifunctor
- Bitraversable.tfst_comp_tsnd
- Bitraversable.tsnd_eq_snd_id'
- Bitraversable.isLawfulTraversable
- Bicompr.bitraverse
- Bitraversable.tfst_comp_tfst
- Bitraversable.tfst_eq_fst_id'
- Bitraversable.traversable
- instBitraversableBicompr
- bisequence
- instLawfulBitraversableBicomplOfLawfulTraversable
- Bitraversable.tsnd_comp_tfst
- Bicompl.bitraverse
- instLawfulBitraversableBicomprOfLawfulTraversable