Instances

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

Statistics

Metric	Count
Definitions bitraverse, bitraverse, const, flip, traversable, bitraverse, bitraverse, bitraverse, bitraverse, instBitraversableBicompl, instBitraversableBicompr, instBitraversableProd, instBitraversableSum	13
Theorems isLawfulTraversable, const, flip, instLawfulBitraversableBicomplOfLawfulTraversable, instLawfulBitraversableBicomprOfLawfulTraversable, instLawfulBitraversableProd, instLawfulBitraversableSum	7
Total	20

Bicompl

Definitions

Name	Category	Theorems
bitraverse 📖	CompOp	—

Bicompr

Definitions

Name	Category	Theorems
bitraverse 📖	CompOp	—

Bitraversable

Definitions

Name	Category	Theorems
const 📖	CompOp	1 math math: LawfulBitraversable.const
flip 📖	CompOp	1 math math: LawfulBitraversable.flip
traversable 📖	CompOp	1 math math: isLawfulTraversable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLawfulTraversable 📖	mathematical	—	LawfulTraversable traversable	—	Bifunctor.lawfulFunctor LawfulBitraversable.toLawfulBifunctor LawfulBitraversable.bitraverse_id_id comp_tsnd tsnd_eq_snd_id LawfulBitraversable.binaturality ApplicativeTransformation.preserves_pure

Const

Definitions

Name	Category	Theorems
bitraverse 📖	CompOp	—

LawfulBitraversable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const 📖	mathematical	—	LawfulBitraversable Functor.Const Bitraversable.const	—	LawfulBifunctor.const
flip 📖	mathematical	—	LawfulBitraversable Bitraversable.flip	—	LawfulBifunctor.flip toLawfulBifunctor

Prod

Definitions

Name	Category	Theorems
bitraverse 📖	CompOp	—

Sum

Definitions

Name	Category	Theorems
bitraverse 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
instBitraversableBicompl 📖	CompOp	1 math math: instLawfulBitraversableBicomplOfLawfulTraversable
instBitraversableBicompr 📖	CompOp	1 math math: instLawfulBitraversableBicomprOfLawfulTraversable
instBitraversableProd 📖	CompOp	1 math math: instLawfulBitraversableProd
instBitraversableSum 📖	CompOp	1 math math: instLawfulBitraversableSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLawfulBitraversableBicomplOfLawfulTraversable 📖	mathematical	—	LawfulBitraversable Function.bicompl instBitraversableBicompl	—	Function.bicompl.lawfulBifunctor LawfulTraversable.toLawfulFunctor LawfulBitraversable.toLawfulBifunctor Traversable.traverse_id LawfulBitraversable.bitraverse_id_id Traversable.traverse_comp LawfulBitraversable.comp_bitraverse Traversable.traverse_eq_map_id' LawfulBitraversable.bitraverse_eq_bimap_id LawfulBitraversable.binaturality Traversable.naturality_pf
instLawfulBitraversableBicomprOfLawfulTraversable 📖	mathematical	—	LawfulBitraversable Function.bicompr instBitraversableBicompr	—	Function.bicompr.lawfulBifunctor LawfulTraversable.toLawfulFunctor LawfulBitraversable.toLawfulBifunctor LawfulBitraversable.bitraverse_id_id LawfulTraversable.id_traverse LawfulBitraversable.bitraverse_comp Traversable.traverse_comp LawfulBitraversable.bitraverse_eq_bimap_id' Traversable.traverse_eq_map_id' LawfulTraversable.naturality LawfulBitraversable.binaturality'
instLawfulBitraversableProd 📖	mathematical	—	LawfulBitraversable instBitraversableProd	—	Prod.lawfulBifunctor CommApplicative.toLawfulApplicative instCommApplicativeId seq_map_assoc map_seq ApplicativeTransformation.preserves_seq ApplicativeTransformation.preserves_map
instLawfulBitraversableSum 📖	mathematical	—	LawfulBitraversable instBitraversableSum	—	Sum.lawfulBifunctor CommApplicative.toLawfulApplicative instCommApplicativeId ApplicativeTransformation.preserves_map

flip

Definitions

Name	Category	Theorems
bitraverse 📖	CompOp	—

---

← Back to Index