Theorems · Theorem

Traversable.comp_sequence

∀ {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {F G : Type u → Type u} [inst_2 : Applicative F]
  [LawfulApplicative F] [inst_4 : Applicative G] [LawfulApplicative G] {α : Type u} (x : t (F (G α))),
  sequence (Functor.Comp.mk <$> x) = Functor.Comp.mk (sequence <$> sequence x)

Defined in

Mathlib.Control.Traversable.Lemmas

Cited by

0 results in Mathlib

Foundations

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

Assumes

TraversableLawfulTraversableApplicativeLawfulApplicativeApplicativeLawfulApplicative