Structures · Data types
Bifunctor
Lawless bifunctor. This typeclass only holds the data for the bimap.
- Defined in
- Mathlib.Control.Bifunctor
- Shape
- One type argument · adds bimap
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Every Bifunctor 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 by28
- Bifunctor.bimap
- Bifunctor.snd
- Bifunctor.fst
- Bifunctor.mapEquiv
- Bifunctor.id_snd
- Bifunctor.snd_fst
- Bifunctor.comp_fst
- Bifunctor.id_fst
- Bifunctor.fst_snd
- Bifunctor.comp_snd
- LawfulBifunctor.flip
- Bifunctor.fst_comp_snd
- Bifunctor.functor
- Bifunctor.snd_id
- Bifunctor.fst_id
- Bifunctor.mapEquiv.congr_simp
- Function.bicompr.bifunctor
- Bifunctor.mapEquiv_symm_apply
- Function.bicompr.lawfulBifunctor
- Bifunctor.mapEquiv_apply
- Function.bicompl.bifunctor
- Bifunctor.snd_comp_fst
- Bifunctor.fst_comp_fst
- Bifunctor.snd_comp_snd
- Bifunctor.mapEquiv_refl_refl
- Bifunctor.lawfulFunctor
- Function.bicompl.lawfulBifunctor
- Bifunctor.flip