Theorems · Theorem

Equiv.traverse_eq_map_id

∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Traversable t] [LawfulTraversable t] {α β : Type u}
  (f : α → β) (x : t' α), Equiv.traverse eqv (pure ∘ f) x = pure (Equiv.map eqv f x)

Defined in

Mathlib.Control.Traversable.Equiv

Cited by

2 results in Mathlib

Foundations

Depth 15 from the axioms · uses Quot.sound

Assumes

TraversableLawfulTraversable