Mokhov is (at least) skew monoidal product, see https://arxiv.org/pdf/1201.4981.pdf

Mokhov.agda

{-# OPTIONS --cubical --type-in-type #-}
module Mokhov where

open import Cubical.Foundations.Everything
open import Cubical.Data.Sum
open import Cubical.Data.Prod
open import Cubical.Data.Unit

record Mokhov (F : Set → Set) (G : Set → Set) (A : Set) : Set where
  constructor mokhov
  field
    X  : Set
    Y  : Set
    h  : X → A ⊎ (Y → A)
    fx : F X
    gy : G Y

private
  variable
    F G H   : Set → Set
    A B C D : Set

record RawFunctor (F : Set → Set) : Set where
  constructor mkFunctor
  field
    fmap : ∀ {A B} → (A → B) → F A → F B

id : ∀ {A : Set} → A → A
id X = X

either : (A → C) → (B → C) → A ⊎ B → C
either f g (inl x) = f x
either f g (inr y) = g y

bimap : (A → C) → (B → D) → A ⊎ B → C ⊎ D
bimap f g (inl x) = inl (f x)
bimap f g (inr y) = inr (g y)

η : G A → Mokhov id G A
η ga = mokhov Unit _ (λ _ → inr id) tt ga

ε : RawFunctor F → Mokhov F id A → F A
ε (mkFunctor F₂) (mokhov _ _ h fx y) = F₂ (λ x → either id (λ z → z y) (h x)) fx

γ : Mokhov F (Mokhov G H) A → Mokhov (Mokhov F G) H A
γ (mokhov X Y i fx (mokhov U V j gu hv)) =
  mokhov _ V id
  (mokhov X U (either (inl ∘ inl) (λ ya → inr (bimap ya (ya ∘_) ∘ j)) ∘ i) fx gu) hv