∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] [toLawfulBifunctor : LawfulBifunctor t],
  (∀ {α β : Type u} (x : t α β), bitraverse pure pure x = pure x) →
    (∀ {F G : Type u → Type u} [inst_1 : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
        [LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
        (x : t α α'),
        bitraverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
          Functor.Comp.mk (bitraverse f f' <$> bitraverse g g' x)) →
      (∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
          bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)) →
        (∀ {F G : Type u → Type u} [inst_1 : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
            [LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β)
            (f' : α' → F β') (x : t α α'),
            (fun {α} => η.app α) (bitraverse f f' x) =
              bitraverse ((fun {α} => η.app α) ∘ f) ((fun {α} => η.app α) ∘ f') x) →
          LawfulBitraversable t