Theorems · Definition · category theory

Bicompr.bitraverse

{t : Type u → Type u → Type u} →
  [Bitraversable t] →
    (F : Type u → Type u) →
      [Traversable F] →
        {m : Type u → Type u} →
          [Applicative m] →
            {α β α' β' : Type u} → (α → m β) → (α' → m β') → Function.bicompr F t α α' → m (Function.bicompr F t β β')

The bitraverse function for bicompr.

Defined in

Mathlib.Control.Bitraversable.Instances

Cited by

0 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

BitraversableTraversableApplicative