deniok

В Agda2 композиция двух функций с обобщённым функциональным типом типизируется так

_○_ : {A : Set}{B : A -> Set}{C : (x : A) -> B x -> Set}
      (f : {x : A}(y : B x) -> C x y)
      (g : (x : A) -> B x)
      (x : A) -> C x (g x)
(f ○ g) x = f (g x)

Укажите теперь тип для "наиболее общей" композиции трёх таких функций

_○₁_○₂_ : ?
(f ○₁ g ○₂ h) x = f (g (h x))

Комменты не скринятся, читеры подвергаются лёгкой форме остракизма :-)

UPD. Ответившего правильно Анонима подержу немного заскриненным.