Equiv

📁 Source: Mathlib/Control/Traversable/Equiv.lean

Statistics

Metric	Count
Definitions functor, map, traversable, traverse	4
Theorems comp_map, comp_traverse, id_map, id_traverse, isLawfulTraversable, isLawfulTraversable', lawfulFunctor, lawfulFunctor', naturality, traverse_def, traverse_eq_map_id	11
Total	15

Equiv

Definitions

Name	Category	Theorems
functor 📖	CompOp	1 math math: lawfulFunctor
map 📖	CompOp	3 math math: traverse_eq_map_id, id_map, comp_map
traversable 📖	CompOp	1 math math: isLawfulTraversable
traverse 📖	CompOp	5 math math: traverse_eq_map_id, traverse_def, id_traverse, comp_traverse, naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_map 📖	mathematical	—	map	—	symm_apply_apply
comp_traverse 📖	mathematical	—	traverse Functor.Comp Functor.Comp.instApplicativeComp	—	traverse_def LawfulTraversable.comp_traverse symm_apply_apply
id_map 📖	mathematical	—	map	—	apply_symm_apply
id_traverse 📖	mathematical	—	traverse	—	traverse.eq_1 LawfulTraversable.id_traverse CommApplicative.toLawfulApplicative instCommApplicativeId apply_symm_apply
isLawfulTraversable 📖	mathematical	—	LawfulTraversable traversable	—	lawfulFunctor LawfulTraversable.toLawfulFunctor id_traverse comp_traverse traverse_eq_map_id naturality
isLawfulTraversable' 📖	mathematical	Traversable.toFunctor map Traversable.traverse traverse	LawfulTraversable	—	lawfulFunctor' LawfulTraversable.toLawfulFunctor CommApplicative.toLawfulApplicative instCommApplicativeId id_traverse Functor.Comp.instLawfulApplicativeComp comp_traverse traverse_eq_map_id naturality
lawfulFunctor 📖	mathematical	—	functor	—	id_map comp_map
lawfulFunctor' 📖	—	map	—	—	lawfulFunctor
naturality 📖	mathematical	—	traverse	—	ApplicativeTransformation.preserves_map LawfulTraversable.naturality
traverse_def 📖	mathematical	—	traverse DFunLike.coe Equiv EquivLike.toFunLike instEquivLike Traversable.traverse symm	—	—
traverse_eq_map_id 📖	mathematical	—	traverse map Traversable.toFunctor	—	LawfulTraversable.traverse_eq_map_id

---

← Back to Index