Theorems · Theorem

Equiv.traverse_def

∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Traversable t] {m : Type u → Type u}
  [inst_1 : Applicative m] {α β : Type u} (f : α → m β) (x : t' α),
  Equiv.traverse eqv f x = ⇑(eqv β) <$> traverse f ((eqv α).symm x)

Defined in

Mathlib.Control.Traversable.Equiv

Cited by

1 results in Mathlib

Foundations

Depth 15 from the axioms · uses Quot.sound

Assumes

TraversableApplicative