Theorems · Theorem

Equiv.isLawfulTraversable

∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Traversable t] [LawfulTraversable t],
  LawfulTraversable t'

The fact that t is a lawful traversable functor carries over the equivalences to t', with the traversable functor structure given by Equiv.traversable.

Defined in

Mathlib.Control.Traversable.Equiv

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound

Assumes

TraversableLawfulTraversable