| ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 x13 : ι → ι . MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ MetaFunctor x4 x5 x6 x7 x0 x1 x2 x3 x10 x11 ⟶ MetaNatTrans x0 x1 x2 x3 x0 x1 x2 x3 (λ x14 . x14) (λ x14 x15 x16 . x16) (λ x14 . x10 (x8 x14)) (λ x14 x15 x16 . x11 (x8 x14) (x8 x15) (x9 x14 x15 x16)) x12 ⟶ MetaNatTrans x4 x5 x6 x7 x4 x5 x6 x7 (λ x14 . x8 (x10 x14)) (λ x14 x15 x16 . x9 (x10 x14) (x10 x15) (x11 x14 x15 x16)) (λ x14 . x14) (λ x14 x15 x16 . x16) x13 ⟶ MetaAdjunction x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ MetaMonad x0 x1 x2 x3 (λ x14 . x10 (x8 x14)) (λ x14 x15 x16 . x11 (x8 x14) (x8 x15) (x9 x14 x15 x16)) x12 (λ x14 . x11 (x8 (x10 (x8 x14))) (x8 x14) (x13 (x8 x14))) |
|