[Agda] Applicative with arbitrary morphisms : how ?

[Permjacov Evgeniy]

let's assume following definitions (record members and parametrs with
laws that must hold are dropped for simplicity)

record categoryOps {oℓ aℓ : Level}
  (obj : Set oℓ)
  (_⇒_ : obj → obj → Set aℓ) : Set (oℓ ⊔ aℓ) where
 field
  id   : {o : obj} → o ⇒ o
  _∘_  : {x y z : obj} → x ⇒ y → y ⇒ z → x ⇒ z

record functorOps {oℓ₁ aℓ₁ oℓ₂ aℓ₂ : Level}
  (obj₁ : Set oℓ₁)
  (_⇒₁_ : obj₁ → obj₁ → Set aℓ₁)
  (cat₁ : categoryOps obj₁ _⇒₁_)
  (obj₂ : Set oℓ₂)
  (_⇒₂_ : obj₂ → obj₂ → Set aℓ₂)
  (cat₂ : categoryOps obj₂ _⇒₂_)
  : Set (oℓ₁ ⊔ aℓ₁ ⊔ oℓ₂ ⊔ aℓ₂) where
 field
  liftO : obj₁ → obj₂
  liftA : {x y : obj₁} → x ⇒₁ y → liftO x ⇒₂ liftO y


monad can be codified with easy as it is simply an endofunctor with two
special types of arrows

record monadOps {oℓ aℓ : Level}
  (obj : Set oℓ)
  (_⇒_ : obj → obj → Set aℓ)
  (cat : categoryOps obj _⇒_)
  (fun : functorOps obj _⇒_ cat obj _⇒_ cat)
  : Set (oℓ ⊔ aℓ) where
 open functorOps fun
 field
  liftV : {o : obj} → o ⇒ liftO o
  join  : {o : obj} → liftO (liftO o) ⇒ liftO o

comonads can be codified in similiar way. However, 'applcative' cannot.
The haskell base uses  function with type

Applicative f => f (a -> b) -> f a -> f b

When I tried to encode this function as f (a =>b) -> f (a) => f (b), I
got typecheck error and it is understandable. A somehow worked (sorry,
no code, I'm rewriting it from scratch) is encoding Combinative, that
will be triple of endofunctor f, two endobifunctors 'ext' and 'int' and
group of morphisms \all {a b} -> ext (f a) (f b) => f (int a b) . This
should typecheck, however, such interface looks extremly heavyweight
from perspective of size of declarations. So, what extension of
functorOps may codify Applicative in sane way ?