Theorems · Theorem

LawfulTraversable.traverse_eq_map_id

∀ {t : Type u → Type u} {inst : Traversable t} [self : LawfulTraversable t] {α β : Type u} (f : α → β) (x : t α),
  traverse (pure ∘ f) x = pure (f <$> x)

An axiom for traverse involving pure : β → Id β.

Defined in

Mathlib.Control.Traversable.Basic

Cited by

3 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

LawfulTraversable