Documentation Verification Report

Basic

📁 Source: Mathlib/Control/Bitraversable/Basic.lean

Statistics

Metric	Count
Definitions `Bitraversable`, `bitraverse`, `toBifunctor`, `LawfulBitraversable`, `bisequence`	5
Theorems `binaturality`, `binaturality'`, `bitraverse_comp`, `bitraverse_eq_bimap_id`, `bitraverse_eq_bimap_id'`, `bitraverse_id_id`, `comp_bitraverse`, `id_bitraverse`, `toLawfulBifunctor`	9
Total	14

Bitraversable

Definitions

Name	Category	Theorems
`bitraverse` 📖	CompOp	12 math math: `LawfulBitraversable.bitraverse_eq_bimap_id`, `LawfulBitraversable.comp_bitraverse`, `tsnd_comp_tfst`, `tfst_tsnd`, `LawfulBitraversable.binaturality`, `LawfulBitraversable.bitraverse_id_id`, `LawfulBitraversable.bitraverse_comp`, `tfst_comp_tsnd`, `tsnd_tfst`, `LawfulBitraversable.bitraverse_eq_bimap_id'`, `LawfulBitraversable.binaturality'`, `LawfulBitraversable.id_bitraverse`
`toBifunctor` 📖	CompOp	7 math math: `LawfulBitraversable.bitraverse_eq_bimap_id`, `LawfulBitraversable.toLawfulBifunctor`, `tsnd_eq_snd_id'`, `tfst_eq_fst_id`, `tsnd_eq_snd_id`, `LawfulBitraversable.bitraverse_eq_bimap_id'`, `tfst_eq_fst_id'`

LawfulBitraversable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`binaturality` 📖	mathematical	—	`Bitraversable.bitraverse`	—	—
`binaturality'` 📖	mathematical	—	`Bitraversable.bitraverse`	—	`binaturality`
`bitraverse_comp` 📖	mathematical	—	`Bitraversable.bitraverse` `Functor.Comp` `Functor.Comp.instApplicativeComp`	—	`comp_bitraverse`
`bitraverse_eq_bimap_id` 📖	mathematical	—	`Bitraversable.bitraverse` `Bifunctor.bimap` `Bitraversable.toBifunctor`	—	—
`bitraverse_eq_bimap_id'` 📖	mathematical	—	`Bitraversable.bitraverse` `Bifunctor.bimap` `Bitraversable.toBifunctor`	—	`bitraverse_eq_bimap_id`
`bitraverse_id_id` 📖	mathematical	—	`Bitraversable.bitraverse`	—	`id_bitraverse`
`comp_bitraverse` 📖	mathematical	—	`Bitraversable.bitraverse` `Functor.Comp` `Functor.Comp.instApplicativeComp`	—	—
`id_bitraverse` 📖	mathematical	—	`Bitraversable.bitraverse`	—	—
`toLawfulBifunctor` 📖	mathematical	—	`LawfulBifunctor` `Bitraversable.toBifunctor`	—	—

(root)

Definitions

Name	Category	Theorems
`Bitraversable` 📖	CompData	—
`LawfulBitraversable` 📖	CompData	6 math math: `instLawfulBitraversableSum`, `instLawfulBitraversableBicomprOfLawfulTraversable`, `LawfulBitraversable.const`, `instLawfulBitraversableBicomplOfLawfulTraversable`, `LawfulBitraversable.flip`, `instLawfulBitraversableProd`
`bisequence` 📖	CompOp	—

---

← Back to Index