Theorems · Definition

Equiv.traverse

{t t' : Type u → Type u} →
  ((α : Type u) → t α ≃ t' α) →
    [Traversable t] → {m : Type u → Type u} → [Applicative m] → {α β : Type u} → (α → m β) → t' α → m (t' β)

Like Equiv.map, a function t' : Type u → Type u can be given the structure of a traversable functor using a traversable functor t' and equivalences t α ≃ t' α for all α. See Equiv.traversable.

Defined in

Mathlib.Control.Traversable.Equiv

Cited by

6 results in Mathlib

Foundations

Depth 14 from the axioms · uses Quot.sound

Assumes

TraversableApplicative